Theorem 3impia 1253

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 449	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1249	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  mopick2  2528  3gencl  3210  vtoclgft  3227  mob2  3353  moi  3356  reupick3  3871  disjne  3974  elpr2elpr  4336  disji2  4569  disji  4570  tz7.2  5022  sofld  5500  ordintdif  5691  funopg  5836  fvun1  6179  fvopab6  6218  fveqressseq  6263  fvcofneq  6275  fprg  6327  isores3  6485  ovmpt4g  6681  ovmpt2s  6682  ov2gf  6683  ofrval  6805  sorpssuni  6844  sorpssint  6845  poxp  7176  suppss2  7216  smoel  7344  smoord  7349  smogt  7351  oaass  7528  oewordi  7558  oeoalem  7563  oeoelem  7565  nnawordi  7588  nnaass  7589  qsel  7713  xpdom3  7943  onsdominel  7994  mapdom3  8017  fisseneq  8056  cantnflem1  8469  cfslbn  8972  cfsmolem  8975  cfcoflem  8977  infpssrlem4  9011  fin23lem7  9021  fin23lem25  9029  isf34lem7  9084  hsmexlem2  9132  axcc3  9143  axdc4lem  9160  tskss  9459  gruss  9497  gruurn  9499  gruiun  9500  gruel  9504  gruen  9513  grudomon  9518  grothac  9531  axpre-sup  9869  axsup  9992  addn0nid  10330  letrp1  10744  p1le  10745  lemul1a  10756  infrelb  10885  zextle  11326  zextlt  11327  btwnnz  11329  gtndiv  11330  uzind2  11346  fzind  11351  eluzsub  11593  zsupss  11653  xrltne  11870  lemaxle  11900  qbtwnre  11904  qbtwnxr  11905  xlemul1a  11990  icogelb  12096  iccleub  12100  iccsplit  12176  uzsubsubfz  12234  elfz0fzfz0  12313  difelfznle  12322  fvffz0  12326  elfzo0le  12379  fzonmapblen  12381  fzofzim  12382  fzosplitprm1  12443  ceile  12510  modadd1  12569  muladdmodid  12572  modmul1  12585  modirr  12603  fsuppmapnn0fiub0  12655  expcl2lem  12734  expclzlem  12746  expnegz  12756  leexp2r  12780  bcval4  12956  bccmpl  12958  hashbnd  12985  elovmpt2wrd  13202  ccatval2  13215  ccatrcl1  13229  wrdl1s1  13247  ccat2s1fvw  13267  swrdsb0eq  13299  swrdccatin1  13334  repswswrd  13382  cshwcsh2id  13425  absexpz  13893  climbdd  14250  iseraltlem2  14261  binomfallfac  14611  dvdsle  14870  divalgb  14965  ndvdssub  14971  dvdsgcd  15099  rplpwr  15114  lcmgcdlem  15157  lcmfunsn  15195  coprmdvds1  15203  qredeq  15209  prmdvdsexpr  15267  nnnn0modprm0  15349  prm23ge5  15358  pcexp  15402  difsqpwdvds  15429  prmpwdvds  15446  ramcl  15571  cshwshashlem3  15642  cshwrepswhash1  15647  elrestr  15912  xpscfv  16045  mreintcl  16078  mremre  16087  mrieqv2d  16122  initoeu2lem1  16487  funcestrcsetclem9  16611  funcsetcestrclem9  16626  prstr  16756  drsdirfi  16761  latnlej  16891  latnlej2  16894  acsdrsel  16990  acsdrscl  16993  mrelatglb  17007  mrelatlub  17009  isnmgm  17069  grpasscan1  17301  grpinvnz  17309  mulgneg2  17398  gsmsymgrfix  17671  f1omvdco2  17691  symggen  17713  odcl2  17805  odhash3  17814  lsmss1  17902  lsmss2  17904  efgred  17984  efgcpbl  17992  ablfacrp  18288  ablfac1eu  18295  ablfaclem3  18309  dvdsrmul1  18476  dvdsunit  18486  irredmul  18532  lmodlema  18691  ply1scln0  19482  psgnodpmr  19755  lindsss  19982  lindfmm  19985  dmatelnd  20121  mdetdiaglem  20223  mdet0  20231  mdetunilem7  20243  slesolinv  20305  cramerimplem3  20310  cpmatpmat  20334  m2cpminvid2lem  20378  chfacfscmul0  20482  chfacfpmmul0  20486  riinopn  20538  clsndisj  20689  cnpf2  20864  hausnei2  20967  cmpcov  21002  cmpfii  21022  uncon  21042  t1conperf  21049  nrmr0reg  21362  fbfinnfr  21455  filuni  21499  alexsubALT  21665  tmdgsum  21709  cuspcvg  21915  mopni  22107  isngp4  22226  metdsre  22464  iimulcl  22544  phtpc01  22604  clmmulg  22709  cfilucfil4  22926  bcthlem5  22933  bcth  22934  bcth3  22936  itg1le  23286  itg2le  23312  bddmulibl  23411  dvnres  23500  cpnord  23504  dvnfre  23521  deg1ge  23662  dgr1term  23820  aaliou3lem2  23902  sincosq1lem  24053  cxpge0  24229  cxpmul2  24235  logrec  24301  sqfpc  24663  bcmono  24802  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem4  24894  2lgsoddprmlem3  24939  pntrmax  25053  qabvexp  25115  ostth2lem2  25123  ax5seglem4  25612  axeuclidlem  25642  uhgredgrnv  25804  edgwlk  26059  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  wwlknimp  26215  wlkiswwlk1  26218  wlkiswwlk2  26225  wwlknext  26252  wwlkextproplem2  26270  wwlkext2clwwlk  26331  erclwwlkeqlen  26340  erclwwlksym  26342  erclwwlktr  26343  erclwwlkneqlen  26352  erclwwlknsym  26354  erclwwlkntr  26355  usg2wotspth  26411  usgfiregdegfi  26438  rusgraprop2  26469  rusgraprop3  26470  rusgranumwlk  26484  4cycl2vnunb  26544  usgn0fidegnn0  26556  nvs  26902  nvtri  26909  nmlno0  27034  nmlnoubi  27035  ubth  27113  hlipgt0  27154  ocnel  27541  elspansn2  27810  elspansn3  27815  normcan  27819  pjoml2  27854  lecm  27860  osum  27888  nmbdfnlb  28293  leopmul  28377  hstpyth  28472  cvnbtwn  28529  ssmd1  28554  ssmd2  28555  ssdmd1  28556  ssdmd2  28557  cvmd  28579  cvdmd  28580  superpos  28597  disji2f  28772  disjif  28773  disjif2  28776  padct  28885  ffs2  28891  bcm1n  28941  omndadd  29037  ogrpaddlt  29049  archiabl  29083  slmdlema  29087  eulerpartlemb  29757  sgn3da  29930  cvmsdisj  30506  cvmlift2lem12  30550  br1steqg  30919  br2ndeqg  30920  poseq  30994  nosepon  31066  nodenselem8  31087  nofulllem4  31104  lineintmo  31434  nn0prpwlem  31487  nn0prpw  31488  neibastop2lem  31525  bddiblnc  32650  areacirc  32675  incsequz  32714  mettrifi  32723  ismtybnd  32776  heiborlem1  32780  rngoisocnv  32950  risci  32956  lfl1  33375  lkrlsp2  33408  omlfh3N  33564  cvrnbtwn  33576  cvrnbtwn2  33580  cvrnbtwn4  33584  cvlexch3  33637  cvlexch4N  33638  cvlatexchb1  33639  2llnne2N  33712  atcvrj0  33732  cvrat2  33733  ps-1  33781  3atlem5  33791  islln2a  33821  lplnriaN  33854  lplnribN  33855  llncvrlpln2  33861  lplncvrlvol2  33919  psubatN  34059  pmapglb2N  34075  pmapglb2xN  34076  2llnma1b  34090  paddasslem17  34140  pmod2iN  34153  pmodl42N  34155  hlmod1i  34160  atmod1i1  34161  atmod1i2  34163  llnmod1i2  34164  pclcmpatN  34205  osumcllem8N  34267  pexmidlem3N  34276  pl42lem4N  34286  4atexlem7  34379  ltrnnid  34440  cdlemc4  34499  cdleme32a  34747  cdlemeg46gfre  34838  cdlemf2  34868  cdlemg4c  34918  trlcoat  35029  tendovalco  35071  tendoeq2  35080  cdlemk36  35219  diael  35350  diatrl  35351  dicelval1stN  35495  dicelval2nd  35496  dihlspsnat  35640  dochkr1  35785  lcfrlem9  35857  mapdh8e  36091  hdmapval0  36143  hgmapval0  36202  incssnn0  36292  pell14qrexpcl  36449  pell14qrgap  36457  congadd  36551  acongsym  36561  acongtr  36563  dvdsacongtr  36569  jm2.19lem3  36576  jm2.19lem4  36577  jm2.26lem3  36586  relexpiidm  37015  bi13impia  37715  3impcombi  38065  ioogtlb  38564  iocgtlb  38571  iocleub  38572  icoltub  38579  iooltub  38582  limclner  38718  iccpartigtl  39961  sqrtpwpw2p  39988  fmtnoprmfac1lem  40014  fmtno4prmfac  40022  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem1  40221  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfx2  40275  pfxccatpfx2  40291  2f1fvneq  40322  elfzelfzlble  40358  subsubelfzo0  40359  usgredg4  40444  nbuhgr2vtx1edgblem  40573  vtxduhgr0e  40693  vtxduhgr0nedg  40707  rusgrpropnb  40783  upgr1wlkwlk  40847  uspgr2wlkeqi  40856  red1wlklem  40880  lfgrwlkprop  40896  2pthnloop  40937  spthonepeq-av  40958  pthdlem2lem  40973  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem7  41019  crctcsh1wlkn0  41024  1wlkiswwlks1  41064  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  wwlksnext  41099  wwlksnextproplem2  41116  wspthsnonn0vne  41124  2pthon3v-av  41150  rusgrnumwwlk  41178  wwlksext2clwwlk  41231  erclwwlkseqlen  41240  erclwwlkssym  41242  erclwwlkstr  41243  erclwwlksneqlen  41252  erclwwlksnsym  41254  erclwwlksntr  41255  uhgr3cyclex  41349  upgreupthseg  41377  eupth2lem3lem4  41399  eucrctshift  41411  4cycl2vnunb-av  41460  c0snmgmhm  41704  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  lincscmcl  42015  lindslinindimp2lem4  42044  lincresunit2  42061  lincresunit3  42064  elfzolborelfzop1  42103  m1modmmod  42110  rege1logbzge0  42151  fllog2  42160  dignn0ldlem  42194