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  2667  ceqsalt  3490  3gencl  3500  vtoclgft  3522  rspc6v  3604  mob2  3680  moi  3683  reupick3  4283  disjne  4415  elpr2elpr  4836  disji2  5095  disji  5096  tz7.2  5646  sofld  6187  ordintdif  6416  funopg  6574  fvun1  6976  fvopab6  7028  fveqressseq  7078  fvcofneq  7092  fprg  7158  isores3  7342  ovmpt4g  7566  ovmpos  7567  ov2gf  7568  ofrval  7696  sorpssuni  7739  sorpssint  7740  poxp  8130  poseq  8160  suppss2  8202  frrlem12  8300  smoel  8353  smoord  8358  smogt  8360  oaass  8552  oewordi  8583  oeoalem  8588  oeoelem  8590  nnawordi  8613  nnaass  8614  naddssim  8678  qsel  8800  xpdom3  9070  onsdominel  9121  mapdom3  9144  sdomdomtrfi  9192  domsdomtrfi  9193  php  9198  onomeneq  9205  fisseneq  9230  fodomfir  9294  cantnflem1  9665  ttrclss  9696  cfslbn  10266  cfsmolem  10269  cfcoflem  10271  infpssrlem4  10305  fin23lem7  10315  fin23lem25  10323  isf34lem7  10378  hsmexlem2  10426  axcc3  10437  axdc4lem  10454  tskss  10758  gruss  10796  gruurn  10798  gruiun  10799  gruel  10803  gruen  10812  grudomon  10817  grothac  10830  axpre-sup  11169  axsup  11300  addn0nid  11649  letrp1  12074  p1le  12075  lemul1a  12084  infrelb  12215  nnadddir  12307  zextle  12685  zextlt  12686  btwnnz  12688  gtndiv  12689  uzind2  12705  fzind  12710  zsupss  12977  xrltne  13204  lemaxle  13237  qbtwnre  13241  qbtwnxr  13242  xlemul1a  13330  icogelb  13439  iccleub  13444  iccsplit  13528  uzsubsubfz  13591  elfz0fzfz0  13678  difelfznle  13687  fvffz0  13691  elfzo0le  13749  fzonmapblen  13754  fzofzim  13755  ceile  13900  modadd1  13959  muladdmodid  13964  modmul1  13978  modirr  13996  fsuppmapnn0fiub0  14047  expcl2lem  14127  expclzlem  14137  expnegz  14150  leexp2r  14228  bcval4  14361  bccmpl  14363  hashbnd  14390  hashunsnggt  14448  hashgt23el  14479  hashfundm  14497  elovmpowrd  14613  ccatval2  14633  ccatrcl1  14651  wrdl1s1  14672  ccat2s1fvw  14696  swrdsb0eq  14723  swrdccatin1  14784  pfxccatpfx2  14796  repswswrd  14845  cshwcsh2id  14889  sgn3da  15162  absexpz  15380  climbdd  15747  iseraltlem2  15758  binomfallfac  16117  dvdsle  16390  divalgb  16484  ndvdssub  16489  dvdsgcd  16624  dfgcd2  16626  rplpwr  16638  nn0rppwr  16641  nn0expgcd  16644  lcmgcdlem  16686  lcmfunsn  16724  coprmdvds1  16732  qredeq  16737  2mulprm  16773  prmdvdsexpr  16798  nnnn0modprm0  16888  prm23ge5  16897  pcexp  16941  difsqpwdvds  16969  prmpwdvds  16986  ramcl  17111  cshwshashlem3  17179  cshwrepswhash1  17184  elrestr  17503  mreintcl  17669  mremre  17678  mrieqv2d  17717  initoeu2lem1  18093  funcestrcsetclem9  18226  funcsetcestrclem9  18241  prstr  18377  drsdirfi  18383  latnlej  18534  latnlej2  18537  acsdrsel  18621  acsdrscl  18624  mrelatglb  18638  mrelatlub  18640  isnmgm  18724  grpasscan1  19112  grpinvnz  19120  mulgneg2  19218  gsmsymgrfix  19542  f1omvdco2  19562  symggen  19584  odcl2  19679  odhash3  19690  lsmss1  19779  lsmss2  19781  efgred  19862  efgcpbl  19870  ablfacrp  20182  ablfac1eu  20189  ablfaclem3  20203  omndadd  20242  ogrpaddlt  20252  dvdsrmul1  20497  dvdsunit  20507  irredmul  20557  c0snmgmhm  20590  lmodlema  21036  psgnodpmr  21790  phlssphl  21859  lindsss  22024  lindfmm  22027  ply1scln0  22502  dmatelnd  22703  mdetdiaglem  22805  mdet0  22813  mdetunilem7  22825  slesolinv  22887  cramerimplem3  22892  cpmatpmat  22917  m2cpminvid2lem  22961  chfacfscmul0  23065  chfacfpmmul0  23069  riinopn  23115  clsndisj  23282  cnpf2  23457  hausnei2  23560  cmpcov  23596  cmpfii  23616  unconn  23636  t1connperf  23643  nrmr0reg  23957  fbfinnfr  24049  filuni  24093  alexsubALT  24259  tmdgsum  24303  cuspcvg  24508  mopni  24700  isngp4  24820  metdsre  25062  iimulcl  25147  phtpc01  25206  clmmulg  25311  cfilucfil4  25531  bcthlem5  25538  bcth  25539  bcth3  25541  itg1le  25923  itg2le  25949  bddmulibl  26049  bddiblnc  26052  dvnres  26141  cpnord  26145  dvnfre  26162  deg1ge  26306  dgr1term  26468  aaliou3lem2  26557  sincosq1lem  26713  cxpge0  26899  cxpmul2  26905  logrec  26979  logbgcd1irr  27010  sqfpc  27352  bcmono  27492  gausslemma2dlem1a  27580  gausslemma2dlem2  27582  gausslemma2dlem4  27584  2lgsoddprmlem3  27629  pntrmax  27779  qabvexp  27841  ostth2lem2  27849  nosepon  27880  nolesgn2o  27886  nogesgn1o  27888  nosepnelem  27894  nosepne  27895  nosepdmlem  27898  nosepdm  27899  nodenselem8  27906  noresle  27912  noetasuplem4  27951  noetainflem4  27955  cutbdaylt  28042  eqcuts3  28048  addsuniflem  28245  sltmuls1  28391  precsexlem6  28456  precsexlem7  28457  precsexlem11  28461  ltonold  28505  onnolt  28510  n0fincut  28599  oldfib  28621  expadds  28679  ax5seglem4  29337  axeuclidlem  29367  uhgredgrnv  29535  usgredg4  29625  nbuhgr2vtx1edgblem  29759  vtxduhgr0e  29886  vtxduhgr0nedg  29900  rusgrpropnb  29991  uspgr2wlkeqi  30055  redwlklem  30077  lfgrwlkprop  30097  2pthnloop  30144  spthonepeq  30165  pthdlem2lem  30180  crctcshwlkn0lem3  30228  crctcshwlkn0lem5  30230  crctcshwlkn0lem7  30232  crctcshwlkn0  30237  wlkiswwlks1  30283  wlkiswwlks2  30291  wlkiswwlksupgr2  30293  wwlksnext  30309  wwlksnextproplem2  30326  wspthsnonn0vne  30333  2pthon3v  30359  rusgrnumwwlk  30394  erclwwlkeqlen  30437  erclwwlksym  30439  erclwwlktr  30440  erclwwlkneqlen  30486  erclwwlknsym  30488  erclwwlkntr  30489  uhgr3cyclex  30604  upgreupthseg  30631  eupth2lem3lem4  30653  eucrctshift  30665  4cycl2vnunb  30712  nvs  31086  nvtri  31093  nmlno0  31218  nmlnoubi  31219  ubth  31296  hlipgt0  31337  ocnel  31721  elspansn2  31990  elspansn3  31995  normcan  31999  pjoml2  32034  lecm  32040  osum  32068  nmbdfnlb  32473  leopmul  32557  hstpyth  32652  cvnbtwn  32709  ssmd1  32734  ssmd2  32735  ssdmd1  32736  ssdmd2  32737  cvmd  32759  cvdmd  32760  superpos  32777  disji2f  32993  disjif  32994  disjif2  32997  preiman0  33126  padct  33133  ffs2  33142  bcm1n  33210  s2f1  33333  archiabl  33582  slmdlema  33587  lbslsat  34070  eulerpartlemb  34823  nelscottrankgt  35576  fisshasheq  35661  cvmsdisj  35799  cvmlift2lem12  35843  satfrel  35896  satfrnmapom  35899  fmlasuc  35915  satffun  35938  satef  35945  sategoelfv  35949  lineintmo  36686  nmuladdss  36742  nn0prpwlem  36890  nn0prpw  36891  neibastop2lem  36928  tr0elw  37052  lindsadd  38321  areacirc  38421  incsequz  38457  mettrifi  38466  ismtybnd  38516  heiborlem1  38520  rngoisocnv  38690  risci  38696  eqvrelqsel  39407  lfl1  39902  lkrlsp2  39935  omlfh3N  40091  cvrnbtwn  40103  cvrnbtwn2  40107  cvrnbtwn4  40111  cvlexch3  40164  cvlexch4N  40165  cvlatexchb1  40166  2llnne2N  40240  atcvrj0  40260  cvrat2  40261  ps-1  40309  3atlem5  40319  islln2a  40349  lplnriaN  40382  lplnribN  40383  llncvrlpln2  40389  lplncvrlvol2  40447  psubatN  40587  pmapglb2N  40603  pmapglb2xN  40604  2llnma1b  40618  paddasslem17  40668  pmod2iN  40681  pmodl42N  40683  hlmod1i  40688  atmod1i1  40689  atmod1i2  40691  llnmod1i2  40692  pclcmpatN  40733  osumcllem8N  40795  pexmidlem3N  40804  pl42lem4N  40814  4atexlem7  40907  ltrnnid  40968  cdlemc4  41026  cdleme32a  41273  cdlemeg46gfre  41364  cdlemf2  41394  cdlemg4c  41444  trlcoat  41555  tendovalco  41597  tendoeq2  41606  cdlemk36  41745  diael  41875  diatrl  41876  dicelval1stN  42020  dicelval2nd  42021  dihlspsnat  42165  dochkr1  42310  lcfrlem9  42382  mapdh8e  42616  hdmapval0  42665  hgmapval0  42724  dvdsexpnn0  43153  incssnn0  43500  pell14qrexpcl  43652  pell14qrgap  43660  congadd  43751  acongsym  43761  acongtr  43763  dvdsacongtr  43769  jm2.19lem3  43776  jm2.19lem4  43777  jm2.26lem3  43786  onexlimgt  44028  nadd2rabex  44171  ismnushort  45069  bi13impia  45256  3impcombi  45583  ioogtlb  46269  iocgtlb  46276  iocleub  46277  icoltub  46282  iooltub  46284  limclner  46423  limsupre3lem  46504  climuzlem  46515  fsupdm  47614  finfdm  47618  elfzelfzlble  48116  subsubelfzo0  48122  m1modnep2mod  48153  m1modmmod  48159  modlt0b  48164  mod2addne  48165  iccpartigtl  48230  sqrtpwpw2p  48348  fmtnoprmfac1lem  48374  fmtno4prmfac  48382  evenltle  48540  even3prm2  48542  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  bgoldbtbndlem1  48628  bgoldbtbndlem3  48630  bgoldbtbndlem4  48631  bgoldbtbnd  48632  uhgrimisgrgriclem  48753  isubgr3stgrlem7  48795  clnbgr3stgrgrlic  48843  gpgedg2iv  48890  pgnbgreunbgrlem3  48941  pgnbgreunbgrlem6  48947  upgrwlkupwlk  48963  funcringcsetcALTV2lem9  49120  funcringcsetclem9ALTV  49143  lincscmcl  49269  lindslinindimp2lem4  49298  lincresunit2  49315  lincresunit3  49318  elfzolborelfzop1  49356  rege1logbzge0  49396  fllog2  49405  dignn0ldlem  49439  rrx2pnecoorneor  49552  rrx2plord2  49559  rrx2linest  49579  ipolub  49823  ipoglb  49826