Theorem 3impia 1135

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 459	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1134	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mopick2  2663  ceqsalt  3484  3gencl  3494  vtoclgft  3516  rspc6v  3597  mob2  3673  moi  3676  reupick3  4276  disjne  4408  elpr2elpr  4829  disji2  5087  disji  5088  tz7.2  5634  sofld  6179  ordintdif  6413  funopg  6572  fvun1  6974  fvopab6  7026  fveqressseq  7077  fvcofneq  7091  fprg  7157  isores3  7341  ovmpt4g  7565  ovmpos  7566  ov2gf  7567  ofrval  7703  sorpssuni  7746  sorpssint  7747  poxp  8138  poseq  8168  suppss2  8210  frrlem12  8308  smoel  8361  smoord  8366  smogt  8368  oaass  8562  oewordi  8593  oeoalem  8598  oeoelem  8600  nnawordi  8623  nnaass  8624  naddssim  8688  qsel  8810  xpdom3  9087  onsdominel  9138  mapdom3  9161  sdomdomtrfi  9209  domsdomtrfi  9210  php  9215  onomeneq  9222  fisseneq  9247  fodomfir  9312  cantnflem1  9683  ttrclss  9714  cfslbn  10338  cfsmolem  10341  cfcoflem  10343  infpssrlem4  10377  fin23lem7  10387  fin23lem25  10395  isf34lem7  10450  hsmexlem2  10498  axcc3  10509  axdc4lem  10526  tskss  10836  gruss  10874  gruurn  10876  gruiun  10877  gruel  10881  gruen  10890  grudomon  10895  grothac  10908  axpre-sup  11247  axsup  11378  addn0nid  11729  letrp1  12154  p1le  12155  lemul1a  12164  infrelb  12295  nnadddir  12387  zextle  12765  zextlt  12766  btwnnz  12768  gtndiv  12769  uzind2  12785  fzind  12790  zsupss  13057  xrltne  13285  lemaxle  13318  qbtwnre  13322  qbtwnxr  13323  xlemul1a  13411  icogelb  13520  iccleub  13525  iccsplit  13609  uzsubsubfz  13673  elfz0fzfz0  13760  difelfznle  13769  fvffz0  13773  elfzo0le  13831  fzonmapblen  13836  fzofzim  13837  ceile  13982  modadd1  14041  muladdmodid  14046  modmul1  14060  modirr  14078  fsuppmapnn0fiub0  14129  expcl2lem  14209  expclzlem  14219  expnegz  14232  leexp2r  14310  bcval4  14444  bccmpl  14446  hashbnd  14473  hashunsnggt  14531  hashgt23el  14562  hashfundm  14580  elovmpowrd  14696  ccatval2  14716  ccatrcl1  14734  wrdl1s1  14755  ccat2s1fvw  14779  swrdsb0eq  14806  swrdccatin1  14867  pfxccatpfx2  14879  repswswrd  14928  cshwcsh2id  14972  sgn3da  15247  absexpz  15465  climbdd  15832  iseraltlem2  15843  binomfallfac  16200  dvdsle  16473  divalgb  16567  ndvdssub  16572  dvdsgcd  16710  dfgcd2  16712  rplpwr  16725  nn0rppwr  16728  nn0expgcd  16731  lcmgcdlem  16774  lcmfunsn  16812  coprmdvds1  16820  qredeq  16825  2mulprm  16861  prmdvdsexpr  16886  nnnn0modprm0  16977  prm23ge5  16986  pcexp  17030  difsqpwdvds  17058  prmpwdvds  17075  ramcl  17200  cshwshashlem3  17268  cshwrepswhash1  17273  elrestr  17592  mreintcl  17758  mremre  17767  mrieqv2d  17806  initoeu2lem1  18182  funcestrcsetclem9  18315  funcsetcestrclem9  18330  prstr  18466  drsdirfi  18472  latnlej  18623  latnlej2  18626  acsdrsel  18710  acsdrscl  18713  mrelatglb  18727  mrelatlub  18729  isnmgm  18813  grpasscan1  19205  grpinvnz  19213  mulgneg2  19311  gsmsymgrfix  19635  f1omvdco2  19655  symggen  19677  odcl2  19772  odhash3  19783  lsmss1  19872  lsmss2  19874  efgred  19955  efgcpbl  19963  ablfacrp  20275  ablfac1eu  20282  ablfaclem3  20296  omndadd  20335  ogrpaddlt  20345  dvdsrmul1  20592  dvdsunit  20602  irredmul  20652  c0snmgmhm  20685  lmodlema  21133  psgnodpmr  21889  phlssphl  21958  lindsss  22123  lindfmm  22126  ply1scln0  22603  dmatelnd  22804  mdetdiaglem  22906  mdet0  22914  mdetunilem7  22926  slesolinv  22991  cramerimplem3  22996  cpmatpmat  23021  m2cpminvid2lem  23065  chfacfscmul0  23169  chfacfpmmul0  23173  riinopn  23219  clsndisj  23386  cnpf2  23561  hausnei2  23664  cmpcov  23700  cmpfii  23720  unconn  23740  t1connperf  23747  nrmr0reg  24061  fbfinnfr  24153  filuni  24197  alexsubALT  24363  tmdgsum  24407  cuspcvg  24612  mopni  24804  isngp4  24924  metdsre  25166  iimulcl  25251  phtpc01  25310  clmmulg  25415  cfilucfil4  25635  bcthlem5  25642  bcth  25643  bcth3  25645  itg1le  26027  itg2le  26053  bddmulibl  26152  bddiblnc  26155  dvnres  26244  cpnord  26248  dvnfre  26265  deg1ge  26409  dgr1term  26572  aaliou3lem2  26663  sincosq1lem  26819  cxpge0  27004  cxpmul2  27010  logrec  27084  logbgcd1irr  27115  sqfpc  27457  bcmono  27597  gausslemma2dlem1a  27685  gausslemma2dlem2  27687  gausslemma2dlem4  27689  2lgsoddprmlem3  27734  pntrmax  27884  qabvexp  27946  ostth2lem2  27954  fltoprmlem2  27987  nosepon  28015  nolesgn2o  28021  nogesgn1o  28023  nosepnelem  28029  nosepne  28030  nosepdmlem  28033  nosepdm  28034  nodenselem8  28041  noresle  28047  noetasuplem4  28086  noetainflem4  28090  cutbdaylt  28177  eqcuts3  28183  addsuniflem  28380  sltmuls1  28526  precsexlem6  28591  precsexlem7  28592  precsexlem11  28596  ltonold  28640  onnolt  28645  n0fincut  28734  oldfib  28756  expadds  28814  ax5seglem4  29503  axeuclidlem  29533  uhgredgrnv  29701  usgredg4  29791  nbuhgr2vtx1edgblem  29925  vtxduhgr0e  30052  vtxduhgr0nedg  30066  rusgrpropnb  30157  uspgr2wlkeqi  30221  redwlklem  30243  lfgrwlkprop  30263  2pthnloop  30310  spthonepeq  30331  pthdlem2lem  30346  crctcshwlkn0lem3  30394  crctcshwlkn0lem5  30396  crctcshwlkn0lem7  30398  crctcshwlkn0  30403  wlkiswwlks1  30449  wlkiswwlks2  30457  wlkiswwlksupgr2  30459  wwlksnext  30475  wwlksnextproplem2  30492  wspthsnonn0vne  30499  2pthon3v  30525  rusgrnumwwlk  30560  erclwwlkeqlen  30603  erclwwlksym  30605  erclwwlktr  30606  erclwwlkneqlen  30652  erclwwlknsym  30654  erclwwlkntr  30655  uhgr3cyclex  30776  upgreupthseg  30803  eupth2lem3lem4  30825  eucrctshift  30837  4cycl2vnunb  30884  nvs  31258  nvtri  31265  nmlno0  31390  nmlnoubi  31391  ubth  31468  hlipgt0  31509  ocnel  31893  elspansn2  32162  elspansn3  32167  normcan  32171  pjoml2  32206  lecm  32212  osum  32240  nmbdfnlb  32645  leopmul  32729  hstpyth  32824  cvnbtwn  32881  ssmd1  32906  ssmd2  32907  ssdmd1  32908  ssdmd2  32909  cvmd  32931  cvdmd  32932  superpos  32949  disji2f  33164  disjif  33165  disjif2  33168  preiman0  33296  padct  33303  ffs2  33312  bcm1n  33380  s2f1  33503  archiabl  33752  slmdlema  33757  lbslsat  34241  eulerpartlemb  34993  nelscottrankgt  35737  fisshasheq  35882  cvmsdisj  36014  cvmlift2lem12  36058  satfrel  36111  satfrnmapom  36114  fmlasuc  36130  satffun  36153  satef  36160  sategoelfv  36164  lineintmo  36902  nmuladdss  36942  nn0prpwlem  37090  nn0prpw  37091  neibastop2lem  37128  tr0elw  37252  lindsadd  38516  areacirc  38611  incsequz  38662  mettrifi  38671  ismtybnd  38721  heiborlem1  38725  rngoisocnv  38895  risci  38901  eqvrelqsel  39612  lfl1  40107  lkrlsp2  40140  omlfh3N  40296  cvrnbtwn  40308  cvrnbtwn2  40312  cvrnbtwn4  40316  cvlexch3  40369  cvlexch4N  40370  cvlatexchb1  40371  2llnne2N  40445  atcvrj0  40465  cvrat2  40466  ps-1  40514  3atlem5  40524  islln2a  40554  lplnriaN  40587  lplnribN  40588  llncvrlpln2  40594  lplncvrlvol2  40652  psubatN  40792  pmapglb2N  40808  pmapglb2xN  40809  2llnma1b  40823  paddasslem17  40873  pmod2iN  40886  pmodl42N  40888  hlmod1i  40893  atmod1i1  40894  atmod1i2  40896  llnmod1i2  40897  pclcmpatN  40938  osumcllem8N  41000  pexmidlem3N  41009  pl42lem4N  41019  4atexlem7  41112  ltrnnid  41173  cdlemc4  41231  cdleme32a  41478  cdlemeg46gfre  41569  cdlemf2  41599  cdlemg4c  41649  trlcoat  41760  tendovalco  41802  tendoeq2  41811  cdlemk36  41950  diael  42080  diatrl  42081  dicelval1stN  42225  dicelval2nd  42226  dihlspsnat  42370  dochkr1  42515  lcfrlem9  42587  mapdh8e  42821  hdmapval0  42870  hgmapval0  42929  dvdsexpnn0  43366  incssnn0  43701  pell14qrexpcl  43853  pell14qrgap  43861  congadd  43952  acongsym  43962  acongtr  43964  dvdsacongtr  43970  jm2.19lem3  43977  jm2.19lem4  43978  jm2.26lem3  43987  onexlimgt  44229  nadd2rabex  44372  ismnushort  45270  bi13impia  45457  3impcombi  45784  ioogtlb  46476  iocgtlb  46483  iocleub  46484  icoltub  46489  iooltub  46491  limclner  46630  limsupre3lem  46711  climuzlem  46722  fsupdm  47821  finfdm  47825  elfzelfzlble  48360  subsubelfzo0  48366  m1modnep2mod  48397  m1modmmod  48403  modlt0b  48408  mod2addne  48409  iccpartigtl  48474  sqrtpwpw2p  48592  fmtnoprmfac1lem  48618  fmtno4prmfac  48626  evenltle  48784  even3prm2  48786  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  bgoldbtbndlem1  48872  bgoldbtbndlem3  48874  bgoldbtbndlem4  48875  bgoldbtbnd  48876  uhgrimisgrgriclem  48997  isubgr3stgrlem7  49039  clnbgr3stgrgrlic  49087  gpgedg2iv  49134  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  upgrwlkupwlk  49207  funcringcsetcALTV2lem9  49364  funcringcsetclem9ALTV  49387  lincscmcl  49513  lindslinindimp2lem4  49542  lincresunit2  49559  lincresunit3  49562  elfzolborelfzop1  49600  rege1logbzge0  49640  fllog2  49649  dignn0ldlem  49683  rrx2pnecoorneor  49796  rrx2plord2  49803  rrx2linest  49823  ipolub  50065  ipoglb  50068