Theorem 3impia 1130

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 457	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1129	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  mopick2  2664  ceqsalt  3487  3gencl  3497  vtoclgft  3520  rspc6v  3602  mob2  3678  moi  3681  reupick3  4282  disjne  4409  elpr2elpr  4827  disji2  5084  disji  5085  tz7.2  5630  sofld  6173  ordintdif  6397  funopg  6555  fvun1  6958  fvopab6  7010  fveqressseq  7060  fvcofneq  7074  fprg  7138  isores3  7319  ovmpt4g  7543  ovmpos  7544  ov2gf  7545  ofrval  7672  sorpssuni  7715  sorpssint  7716  poxp  8108  poseq  8138  suppss2  8180  frrlem12  8278  smoel  8331  smoord  8336  smogt  8338  oaass  8530  oewordi  8561  oeoalem  8566  oeoelem  8568  nnawordi  8591  nnaass  8592  naddssim  8656  qsel  8778  xpdom3  9047  onsdominel  9098  mapdom3  9121  sdomdomtrfi  9169  domsdomtrfi  9170  php  9175  onomeneq  9182  fisseneq  9207  fodomfir  9272  cantnflem1  9644  ttrclss  9675  cfslbn  10224  cfsmolem  10227  cfcoflem  10229  infpssrlem4  10263  fin23lem7  10273  fin23lem25  10281  isf34lem7  10336  hsmexlem2  10384  axcc3  10395  axdc4lem  10412  tskss  10716  gruss  10754  gruurn  10756  gruiun  10757  gruel  10761  gruen  10770  grudomon  10775  grothac  10788  axpre-sup  11127  axsup  11258  addn0nid  11607  letrp1  12035  p1le  12036  lemul1a  12045  infrelb  12177  nnadddir  12269  zextle  12646  zextlt  12647  btwnnz  12649  gtndiv  12650  uzind2  12666  fzind  12671  zsupss  12938  xrltne  13165  lemaxle  13198  qbtwnre  13202  qbtwnxr  13203  xlemul1a  13291  icogelb  13400  iccleub  13405  iccsplit  13489  uzsubsubfz  13551  elfz0fzfz0  13638  difelfznle  13647  fvffz0  13651  elfzo0le  13709  fzonmapblen  13714  fzofzim  13715  ceile  13859  modadd1  13918  muladdmodid  13923  modmul1  13937  modirr  13955  fsuppmapnn0fiub0  14006  expcl2lem  14086  expclzlem  14096  expnegz  14109  leexp2r  14187  bcval4  14320  bccmpl  14322  hashbnd  14349  hashunsnggt  14407  hashgt23el  14437  hashfundm  14455  elovmpowrd  14571  ccatval2  14591  ccatrcl1  14608  wrdl1s1  14628  ccat2s1fvw  14652  swrdsb0eq  14677  swrdccatin1  14738  pfxccatpfx2  14750  repswswrd  14797  cshwcsh2id  14841  sgn3da  15114  absexpz  15332  climbdd  15699  iseraltlem2  15710  binomfallfac  16071  dvdsle  16344  divalgb  16438  ndvdssub  16443  dvdsgcd  16578  dfgcd2  16580  rplpwr  16592  nn0rppwr  16595  nn0expgcd  16598  lcmgcdlem  16640  lcmfunsn  16678  coprmdvds1  16686  qredeq  16691  2mulprm  16727  prmdvdsexpr  16752  nnnn0modprm0  16842  prm23ge5  16851  pcexp  16895  difsqpwdvds  16923  prmpwdvds  16940  ramcl  17065  cshwshashlem3  17133  cshwrepswhash1  17138  elrestr  17457  mreintcl  17623  mremre  17632  mrieqv2d  17671  initoeu2lem1  18047  funcestrcsetclem9  18180  funcsetcestrclem9  18195  prstr  18331  drsdirfi  18337  latnlej  18488  latnlej2  18491  acsdrsel  18575  acsdrscl  18578  mrelatglb  18592  mrelatlub  18594  isnmgm  18678  grpasscan1  19043  grpinvnz  19052  mulgneg2  19150  gsmsymgrfix  19468  f1omvdco2  19488  symggen  19510  odcl2  19605  odhash3  19616  lsmss1  19705  lsmss2  19707  efgred  19788  efgcpbl  19796  ablfacrp  20108  ablfac1eu  20115  ablfaclem3  20129  omndadd  20168  ogrpaddlt  20178  dvdsrmul1  20414  dvdsunit  20424  irredmul  20474  c0snmgmhm  20507  lmodlema  20929  psgnodpmr  21639  phlssphl  21708  lindsss  21873  lindfmm  21876  ply1scln0  22351  dmatelnd  22553  mdetdiaglem  22655  mdet0  22663  mdetunilem7  22675  slesolinv  22737  cramerimplem3  22742  cpmatpmat  22767  m2cpminvid2lem  22811  chfacfscmul0  22915  chfacfpmmul0  22919  riinopn  22965  clsndisj  23132  cnpf2  23307  hausnei2  23410  cmpcov  23446  cmpfii  23466  unconn  23486  t1connperf  23493  nrmr0reg  23806  fbfinnfr  23898  filuni  23942  alexsubALT  24108  tmdgsum  24152  cuspcvg  24357  mopni  24549  isngp4  24669  metdsre  24911  iimulcl  24996  phtpc01  25055  clmmulg  25160  cfilucfil4  25380  bcthlem5  25387  bcth  25388  bcth3  25390  itg1le  25772  itg2le  25798  bddmulibl  25898  bddiblnc  25901  dvnres  25990  cpnord  25994  dvnfre  26011  deg1ge  26155  dgr1term  26317  aaliou3lem2  26404  sincosq1lem  26559  cxpge0  26745  cxpmul2  26751  logrec  26825  logbgcd1irr  26856  sqfpc  27198  bcmono  27338  gausslemma2dlem1a  27426  gausslemma2dlem2  27428  gausslemma2dlem4  27430  2lgsoddprmlem3  27475  pntrmax  27625  qabvexp  27687  ostth2lem2  27695  nosepon  27726  nolesgn2o  27732  nogesgn1o  27734  nosepnelem  27740  nosepne  27741  nosepdmlem  27744  nosepdm  27745  nodenselem8  27752  noresle  27758  noetasuplem4  27797  noetainflem4  27801  cutbdaylt  27888  eqcuts3  27894  addsuniflem  28091  sltmuls1  28237  precsexlem6  28302  precsexlem7  28303  precsexlem11  28307  ltonold  28351  onnolt  28356  n0fincut  28445  oldfib  28467  expadds  28525  ax5seglem4  29130  axeuclidlem  29160  uhgredgrnv  29328  usgredg4  29415  nbuhgr2vtx1edgblem  29549  vtxduhgr0e  29676  vtxduhgr0nedg  29690  rusgrpropnb  29781  uspgr2wlkeqi  29845  redwlklem  29867  lfgrwlkprop  29883  2pthnloop  29928  spthonepeq  29949  pthdlem2lem  29964  crctcshwlkn0lem3  30009  crctcshwlkn0lem5  30011  crctcshwlkn0lem7  30013  crctcshwlkn0  30018  wlkiswwlks1  30064  wlkiswwlks2  30072  wlkiswwlksupgr2  30074  wwlksnext  30090  wwlksnextproplem2  30107  wspthsnonn0vne  30114  2pthon3v  30140  rusgrnumwwlk  30175  erclwwlkeqlen  30218  erclwwlksym  30220  erclwwlktr  30221  erclwwlkneqlen  30267  erclwwlknsym  30269  erclwwlkntr  30270  uhgr3cyclex  30381  upgreupthseg  30408  eupth2lem3lem4  30430  eucrctshift  30442  4cycl2vnunb  30489  nvs  30863  nvtri  30870  nmlno0  30995  nmlnoubi  30996  ubth  31073  hlipgt0  31114  ocnel  31498  elspansn2  31767  elspansn3  31772  normcan  31776  pjoml2  31811  lecm  31817  osum  31845  nmbdfnlb  32250  leopmul  32334  hstpyth  32429  cvnbtwn  32486  ssmd1  32511  ssmd2  32512  ssdmd1  32513  ssdmd2  32514  cvmd  32536  cvdmd  32537  superpos  32554  disji2f  32774  disjif  32775  disjif2  32778  preiman0  32909  padct  32917  ffs2  32926  bcm1n  32994  s2f1  33120  archiabl  33375  slmdlema  33380  lbslsat  33910  eulerpartlemb  34662  fisshasheq  35462  cvmsdisj  35617  cvmlift2lem12  35661  satfrel  35714  satfrnmapom  35717  fmlasuc  35733  satffun  35756  satef  35763  sategoelfv  35767  lineintmo  36504  nn0prpwlem  36679  nn0prpw  36680  neibastop2lem  36717  tr0elw  36841  lindsadd  38109  areacirc  38209  incsequz  38244  mettrifi  38253  ismtybnd  38303  heiborlem1  38307  rngoisocnv  38477  risci  38483  eqvrelqsel  39196  lfl1  39691  lkrlsp2  39724  omlfh3N  39880  cvrnbtwn  39892  cvrnbtwn2  39896  cvrnbtwn4  39900  cvlexch3  39953  cvlexch4N  39954  cvlatexchb1  39955  2llnne2N  40029  atcvrj0  40049  cvrat2  40050  ps-1  40098  3atlem5  40108  islln2a  40138  lplnriaN  40171  lplnribN  40172  llncvrlpln2  40178  lplncvrlvol2  40236  psubatN  40376  pmapglb2N  40392  pmapglb2xN  40393  2llnma1b  40407  paddasslem17  40457  pmod2iN  40470  pmodl42N  40472  hlmod1i  40477  atmod1i1  40478  atmod1i2  40480  llnmod1i2  40481  pclcmpatN  40522  osumcllem8N  40584  pexmidlem3N  40593  pl42lem4N  40603  4atexlem7  40696  ltrnnid  40757  cdlemc4  40815  cdleme32a  41062  cdlemeg46gfre  41153  cdlemf2  41183  cdlemg4c  41233  trlcoat  41344  tendovalco  41386  tendoeq2  41395  cdlemk36  41534  diael  41664  diatrl  41665  dicelval1stN  41809  dicelval2nd  41810  dihlspsnat  41954  dochkr1  42099  lcfrlem9  42171  mapdh8e  42405  hdmapval0  42454  hgmapval0  42513  dvdsexpnn0  42940  incssnn0  43289  pell14qrexpcl  43441  pell14qrgap  43449  congadd  43540  acongsym  43550  acongtr  43552  dvdsacongtr  43558  jm2.19lem3  43565  jm2.19lem4  43566  jm2.26lem3  43575  onexlimgt  43817  nadd2rabex  43960  ismnushort  44874  bi13impia  45062  3impcombi  45389  ioogtlb  46068  iocgtlb  46075  iocleub  46076  icoltub  46081  iooltub  46083  limclner  46222  limsupre3lem  46303  climuzlem  46314  fsupdm  47413  finfdm  47417  elfzelfzlble  47912  subsubelfzo0  47918  m1modnep2mod  47949  m1modmmod  47955  modlt0b  47960  mod2addne  47961  iccpartigtl  48026  sqrtpwpw2p  48144  fmtnoprmfac1lem  48170  fmtno4prmfac  48178  evenltle  48336  even3prm2  48338  wtgoldbnnsum4prm  48421  bgoldbnnsum3prm  48423  bgoldbtbndlem1  48424  bgoldbtbndlem3  48426  bgoldbtbndlem4  48427  bgoldbtbnd  48428  uhgrimisgrgriclem  48549  isubgr3stgrlem7  48591  clnbgr3stgrgrlic  48639  gpgedg2iv  48686  pgnbgreunbgrlem3  48737  pgnbgreunbgrlem6  48743  upgrwlkupwlk  48759  funcringcsetcALTV2lem9  48917  funcringcsetclem9ALTV  48940  lincscmcl  49051  lindslinindimp2lem4  49080  lincresunit2  49097  lincresunit3  49100  elfzolborelfzop1  49138  rege1logbzge0  49178  fllog2  49187  dignn0ldlem  49221  rrx2pnecoorneor  49334  rrx2plord2  49341  rrx2linest  49361  ipolub  49606  ipoglb  49609