Theorem 3impia 1117

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mopick2  2637  ceqsalt  3474  3gencl  3484  vtoclgft  3509  vtoclegft  3543  rspc6v  3597  mob2  3673  moi  3676  reupick3  4282  disjne  4407  elpr2elpr  4825  disji2  5082  disji  5083  tz7.2  5607  sofld  6145  ordintdif  6368  funopg  6526  fvun1  6925  fvopab6  6975  fveqressseq  7024  fvcofneq  7038  fprg  7100  isores3  7281  ovmpt4g  7505  ovmpos  7506  ov2gf  7507  ofrval  7634  sorpssuni  7677  sorpssint  7678  poxp  8070  poseq  8100  suppss2  8142  frrlem12  8239  smoel  8292  smoord  8297  smogt  8299  oaass  8488  oewordi  8519  oeoalem  8524  oeoelem  8526  nnawordi  8549  nnaass  8550  naddssim  8613  qsel  8733  xpdom3  9003  onsdominel  9054  mapdom3  9077  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  onomeneq  9138  fisseneq  9163  fodomfir  9228  cantnflem1  9598  ttrclss  9629  cfslbn  10177  cfsmolem  10180  cfcoflem  10182  infpssrlem4  10216  fin23lem7  10226  fin23lem25  10234  isf34lem7  10289  hsmexlem2  10337  axcc3  10348  axdc4lem  10365  tskss  10669  gruss  10707  gruurn  10709  gruiun  10710  gruel  10714  gruen  10723  grudomon  10728  grothac  10741  axpre-sup  11080  axsup  11208  addn0nid  11557  letrp1  11985  p1le  11986  lemul1a  11995  infrelb  12127  zextle  12565  zextlt  12566  btwnnz  12568  gtndiv  12569  uzind2  12585  fzind  12590  zsupss  12850  xrltne  13077  lemaxle  13110  qbtwnre  13114  qbtwnxr  13115  xlemul1a  13203  icogelb  13312  iccleub  13317  iccsplit  13401  uzsubsubfz  13462  elfz0fzfz0  13549  difelfznle  13558  fvffz0  13562  elfzo0le  13619  fzonmapblen  13624  fzofzim  13625  ceile  13769  modadd1  13828  muladdmodid  13833  modmul1  13847  modirr  13865  fsuppmapnn0fiub0  13916  expcl2lem  13996  expclzlem  14006  expnegz  14019  leexp2r  14097  bcval4  14230  bccmpl  14232  hashbnd  14259  hashunsnggt  14317  hashgt23el  14347  hashfundm  14365  elovmpowrd  14481  ccatval2  14501  ccatrcl1  14518  wrdl1s1  14538  ccat2s1fvw  14562  swrdsb0eq  14587  swrdccatin1  14648  pfxccatpfx2  14660  repswswrd  14707  cshwcsh2id  14751  absexpz  15228  climbdd  15595  iseraltlem2  15606  binomfallfac  15964  dvdsle  16237  divalgb  16331  ndvdssub  16336  dvdsgcd  16471  dfgcd2  16473  rplpwr  16485  nn0rppwr  16488  nn0expgcd  16491  lcmgcdlem  16533  lcmfunsn  16571  coprmdvds1  16579  qredeq  16584  2mulprm  16620  prmdvdsexpr  16644  nnnn0modprm0  16734  prm23ge5  16743  pcexp  16787  difsqpwdvds  16815  prmpwdvds  16832  ramcl  16957  cshwshashlem3  17025  cshwrepswhash1  17030  elrestr  17348  mreintcl  17514  mremre  17523  mrieqv2d  17562  initoeu2lem1  17938  funcestrcsetclem9  18071  funcsetcestrclem9  18086  prstr  18222  drsdirfi  18228  latnlej  18379  latnlej2  18382  acsdrsel  18466  acsdrscl  18469  mrelatglb  18483  mrelatlub  18485  isnmgm  18569  grpasscan1  18931  grpinvnz  18940  mulgneg2  19038  gsmsymgrfix  19357  f1omvdco2  19377  symggen  19399  odcl2  19494  odhash3  19505  lsmss1  19594  lsmss2  19596  efgred  19677  efgcpbl  19685  ablfacrp  19997  ablfac1eu  20004  ablfaclem3  20018  omndadd  20057  ogrpaddlt  20067  dvdsrmul1  20305  dvdsunit  20315  irredmul  20365  c0snmgmhm  20398  lmodlema  20816  psgnodpmr  21545  phlssphl  21614  lindsss  21779  lindfmm  21782  ply1scln0  22234  dmatelnd  22440  mdetdiaglem  22542  mdet0  22550  mdetunilem7  22562  slesolinv  22624  cramerimplem3  22629  cpmatpmat  22654  m2cpminvid2lem  22698  chfacfscmul0  22802  chfacfpmmul0  22806  riinopn  22852  clsndisj  23019  cnpf2  23194  hausnei2  23297  cmpcov  23333  cmpfii  23353  unconn  23373  t1connperf  23380  nrmr0reg  23693  fbfinnfr  23785  filuni  23829  alexsubALT  23995  tmdgsum  24039  cuspcvg  24244  mopni  24436  isngp4  24556  metdsre  24798  iimulcl  24889  phtpc01  24951  clmmulg  25057  cfilucfil4  25277  bcthlem5  25284  bcth  25285  bcth3  25287  itg1le  25670  itg2le  25696  bddmulibl  25796  bddiblnc  25799  dvnres  25889  cpnord  25893  dvnfre  25912  deg1ge  26059  dgr1term  26221  aaliou3lem2  26307  sincosq1lem  26462  cxpge0  26648  cxpmul2  26654  logrec  26729  logbgcd1irr  26760  sqfpc  27103  bcmono  27244  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem4  27336  2lgsoddprmlem3  27381  pntrmax  27531  qabvexp  27593  ostth2lem2  27601  nosepon  27633  nolesgn2o  27639  nogesgn1o  27641  nosepnelem  27647  nosepne  27648  nosepdmlem  27651  nosepdm  27652  nodenselem8  27659  noresle  27665  noetasuplem4  27704  noetainflem4  27708  cutbdaylt  27794  eqcuts3  27800  addsuniflem  27997  sltmuls1  28143  precsexlem6  28208  precsexlem7  28209  precsexlem11  28213  ltonold  28257  onnolt  28262  n0fincut  28351  oldfib  28373  expadds  28431  ax5seglem4  29005  axeuclidlem  29035  uhgredgrnv  29203  usgredg4  29290  nbuhgr2vtx1edgblem  29424  vtxduhgr0e  29552  vtxduhgr0nedg  29566  rusgrpropnb  29657  uspgr2wlkeqi  29721  redwlklem  29743  lfgrwlkprop  29759  2pthnloop  29804  spthonepeq  29825  pthdlem2lem  29840  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  crctcshwlkn0lem7  29889  crctcshwlkn0  29894  wlkiswwlks1  29940  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wwlksnext  29966  wwlksnextproplem2  29983  wspthsnonn0vne  29990  2pthon3v  30016  rusgrnumwwlk  30051  erclwwlkeqlen  30094  erclwwlksym  30096  erclwwlktr  30097  erclwwlkneqlen  30143  erclwwlknsym  30145  erclwwlkntr  30146  uhgr3cyclex  30257  upgreupthseg  30284  eupth2lem3lem4  30306  eucrctshift  30318  4cycl2vnunb  30365  nvs  30738  nvtri  30745  nmlno0  30870  nmlnoubi  30871  ubth  30948  hlipgt0  30989  ocnel  31373  elspansn2  31642  elspansn3  31647  normcan  31651  pjoml2  31686  lecm  31692  osum  31720  nmbdfnlb  32125  leopmul  32209  hstpyth  32304  cvnbtwn  32361  ssmd1  32386  ssmd2  32387  ssdmd1  32388  ssdmd2  32389  cvmd  32411  cvdmd  32412  superpos  32429  disji2f  32652  disjif  32653  disjif2  32656  preiman0  32789  padct  32797  ffs2  32806  bcm1n  32875  sgn3da  32915  s2f1  33027  archiabl  33280  slmdlema  33285  lbslsat  33773  eulerpartlemb  34525  fisshasheq  35309  cvmsdisj  35464  cvmlift2lem12  35508  satfrel  35561  satfrnmapom  35564  fmlasuc  35580  satffun  35603  satef  35610  sategoelfv  35614  lineintmo  36351  nn0prpwlem  36516  nn0prpw  36517  neibastop2lem  36554  lindsadd  37814  areacirc  37914  incsequz  37949  mettrifi  37958  ismtybnd  38008  heiborlem1  38012  rngoisocnv  38182  risci  38188  eqvrelqsel  38873  lfl1  39330  lkrlsp2  39363  omlfh3N  39519  cvrnbtwn  39531  cvrnbtwn2  39535  cvrnbtwn4  39539  cvlexch3  39592  cvlexch4N  39593  cvlatexchb1  39594  2llnne2N  39668  atcvrj0  39688  cvrat2  39689  ps-1  39737  3atlem5  39747  islln2a  39777  lplnriaN  39810  lplnribN  39811  llncvrlpln2  39817  lplncvrlvol2  39875  psubatN  40015  pmapglb2N  40031  pmapglb2xN  40032  2llnma1b  40046  paddasslem17  40096  pmod2iN  40109  pmodl42N  40111  hlmod1i  40116  atmod1i1  40117  atmod1i2  40119  llnmod1i2  40120  pclcmpatN  40161  osumcllem8N  40223  pexmidlem3N  40232  pl42lem4N  40242  4atexlem7  40335  ltrnnid  40396  cdlemc4  40454  cdleme32a  40701  cdlemeg46gfre  40792  cdlemf2  40822  cdlemg4c  40872  trlcoat  40983  tendovalco  41025  tendoeq2  41034  cdlemk36  41173  diael  41303  diatrl  41304  dicelval1stN  41448  dicelval2nd  41449  dihlspsnat  41593  dochkr1  41738  lcfrlem9  41810  mapdh8e  42044  hdmapval0  42093  hgmapval0  42152  nnadddir  42525  dvdsexpnn0  42589  incssnn0  42953  pell14qrexpcl  43109  pell14qrgap  43117  congadd  43208  acongsym  43218  acongtr  43220  dvdsacongtr  43226  jm2.19lem3  43233  jm2.19lem4  43234  jm2.26lem3  43243  onexlimgt  43485  nadd2rabex  43628  ismnushort  44542  bi13impia  44730  3impcombi  45057  ioogtlb  45741  iocgtlb  45748  iocleub  45749  icoltub  45754  iooltub  45756  limclner  45895  limsupre3lem  45976  climuzlem  45987  fsupdm  47086  finfdm  47090  elfzelfzlble  47567  subsubelfzo0  47572  m1modnep2mod  47598  m1modmmod  47604  modlt0b  47609  mod2addne  47610  iccpartigtl  47669  sqrtpwpw2p  47784  fmtnoprmfac1lem  47810  fmtno4prmfac  47818  evenltle  47963  even3prm2  47965  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem1  48051  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  uhgrimisgrgriclem  48176  isubgr3stgrlem7  48218  clnbgr3stgrgrlic  48266  gpgedg2iv  48313  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  upgrwlkupwlk  48386  funcringcsetcALTV2lem9  48544  funcringcsetclem9ALTV  48567  lincscmcl  48678  lindslinindimp2lem4  48707  lincresunit2  48724  lincresunit3  48727  elfzolborelfzop1  48765  rege1logbzge0  48805  fllog2  48814  dignn0ldlem  48848  rrx2pnecoorneor  48961  rrx2plord2  48968  rrx2linest  48988  ipolub  49233  ipoglb  49236