Theorem 3impia 1118

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 1117	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  mopick2  2637  ceqsalt  3515  3gencl  3525  vtoclgft  3552  vtoclegft  3588  rspc6v  3643  mob2  3721  moi  3724  reupick3  4330  disjne  4455  elpr2elpr  4869  disji2  5127  disji  5128  tz7.2  5668  sofld  6207  ordintdif  6434  funopg  6600  fvun1  7000  fvopab6  7050  fveqressseq  7099  fvcofneq  7113  fprg  7175  2f1fvneq  7280  isores3  7355  ovmpt4g  7580  ovmpos  7581  ov2gf  7582  ofrval  7709  sorpssuni  7752  sorpssint  7753  poxp  8153  poseq  8183  suppss2  8225  frrlem12  8322  smoel  8400  smoord  8405  smogt  8407  oaass  8599  oewordi  8629  oeoalem  8634  oeoelem  8636  nnawordi  8659  nnaass  8660  naddssim  8723  qsel  8836  xpdom3  9110  onsdominel  9166  mapdom3  9189  sdomdomtrfi  9241  domsdomtrfi  9242  php  9247  onomeneq  9265  fisseneq  9293  fodomfir  9368  cantnflem1  9729  ttrclss  9760  cfslbn  10307  cfsmolem  10310  cfcoflem  10312  infpssrlem4  10346  fin23lem7  10356  fin23lem25  10364  isf34lem7  10419  hsmexlem2  10467  axcc3  10478  axdc4lem  10495  tskss  10798  gruss  10836  gruurn  10838  gruiun  10839  gruel  10843  gruen  10852  grudomon  10857  grothac  10870  axpre-sup  11209  axsup  11336  addn0nid  11683  letrp1  12111  p1le  12112  lemul1a  12121  infrelb  12253  zextle  12691  zextlt  12692  btwnnz  12694  gtndiv  12695  uzind2  12711  fzind  12716  eluzsubOLD  12914  zsupss  12979  xrltne  13205  lemaxle  13237  qbtwnre  13241  qbtwnxr  13242  xlemul1a  13330  icogelb  13438  iccleub  13442  iccsplit  13525  uzsubsubfz  13586  elfz0fzfz0  13673  difelfznle  13682  fvffz0  13686  elfzo0le  13743  fzonmapblen  13748  fzofzim  13749  ceile  13889  modadd1  13948  muladdmodid  13951  modmul1  13965  modirr  13983  fsuppmapnn0fiub0  14034  expcl2lem  14114  expclzlem  14124  expnegz  14137  leexp2r  14214  bcval4  14346  bccmpl  14348  hashbnd  14375  hashunsnggt  14433  hashgt23el  14463  hashfundm  14481  elovmpowrd  14596  ccatval2  14616  ccatrcl1  14632  wrdl1s1  14652  ccat2s1fvw  14676  swrdsb0eq  14701  swrdccatin1  14763  pfxccatpfx2  14775  repswswrd  14822  cshwcsh2id  14867  absexpz  15344  climbdd  15708  iseraltlem2  15719  binomfallfac  16077  dvdsle  16347  divalgb  16441  ndvdssub  16446  dvdsgcd  16581  dfgcd2  16583  rplpwr  16595  nn0rppwr  16598  nn0expgcd  16601  lcmgcdlem  16643  lcmfunsn  16681  coprmdvds1  16689  qredeq  16694  2mulprm  16730  prmdvdsexpr  16754  nnnn0modprm0  16844  prm23ge5  16853  pcexp  16897  difsqpwdvds  16925  prmpwdvds  16942  ramcl  17067  cshwshashlem3  17135  cshwrepswhash1  17140  elrestr  17473  mreintcl  17638  mremre  17647  mrieqv2d  17682  initoeu2lem1  18059  funcestrcsetclem9  18193  funcsetcestrclem9  18208  prstr  18345  drsdirfi  18351  latnlej  18501  latnlej2  18504  acsdrsel  18588  acsdrscl  18591  mrelatglb  18605  mrelatlub  18607  isnmgm  18657  grpasscan1  19019  grpinvnz  19028  mulgneg2  19126  gsmsymgrfix  19446  f1omvdco2  19466  symggen  19488  odcl2  19583  odhash3  19594  lsmss1  19683  lsmss2  19685  efgred  19766  efgcpbl  19774  ablfacrp  20086  ablfac1eu  20093  ablfaclem3  20107  dvdsrmul1  20369  dvdsunit  20379  irredmul  20429  c0snmgmhm  20462  lmodlema  20863  psgnodpmr  21608  phlssphl  21677  lindsss  21844  lindfmm  21847  ply1scln0  22295  dmatelnd  22502  mdetdiaglem  22604  mdet0  22612  mdetunilem7  22624  slesolinv  22686  cramerimplem3  22691  cpmatpmat  22716  m2cpminvid2lem  22760  chfacfscmul0  22864  chfacfpmmul0  22868  riinopn  22914  clsndisj  23083  cnpf2  23258  hausnei2  23361  cmpcov  23397  cmpfii  23417  unconn  23437  t1connperf  23444  nrmr0reg  23757  fbfinnfr  23849  filuni  23893  alexsubALT  24059  tmdgsum  24103  cuspcvg  24310  mopni  24505  isngp4  24625  metdsre  24875  iimulcl  24966  phtpc01  25028  clmmulg  25134  cfilucfil4  25355  bcthlem5  25362  bcth  25363  bcth3  25365  itg1le  25748  itg2le  25774  bddmulibl  25874  bddiblnc  25877  dvnres  25967  cpnord  25971  dvnfre  25990  deg1ge  26137  dgr1term  26299  aaliou3lem2  26385  sincosq1lem  26539  cxpge0  26725  cxpmul2  26731  logrec  26806  logbgcd1irr  26837  sqfpc  27180  bcmono  27321  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem4  27413  2lgsoddprmlem3  27458  pntrmax  27608  qabvexp  27670  ostth2lem2  27678  nosepon  27710  nolesgn2o  27716  nogesgn1o  27718  nosepnelem  27724  nosepne  27725  nosepdmlem  27728  nosepdm  27729  nodenselem8  27736  noresle  27742  noetasuplem4  27781  noetainflem4  27785  scutbdaylt  27863  addsuniflem  28034  ssltmul1  28173  precsexlem6  28236  precsexlem7  28237  precsexlem11  28241  sltonold  28283  ax5seglem4  28947  axeuclidlem  28977  uhgredgrnv  29147  usgredg4  29234  nbuhgr2vtx1edgblem  29368  vtxduhgr0e  29496  vtxduhgr0nedg  29510  rusgrpropnb  29601  uspgr2wlkeqi  29666  redwlklem  29689  lfgrwlkprop  29705  2pthnloop  29751  spthonepeq  29772  pthdlem2lem  29787  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  crctcshwlkn0lem7  29836  crctcshwlkn0  29841  wlkiswwlks1  29887  wlkiswwlks2  29895  wlkiswwlksupgr2  29897  wwlksnext  29913  wwlksnextproplem2  29930  wspthsnonn0vne  29937  2pthon3v  29963  rusgrnumwwlk  29995  erclwwlkeqlen  30038  erclwwlksym  30040  erclwwlktr  30041  erclwwlkneqlen  30087  erclwwlknsym  30089  erclwwlkntr  30090  uhgr3cyclex  30201  upgreupthseg  30228  eupth2lem3lem4  30250  eucrctshift  30262  4cycl2vnunb  30309  nvs  30682  nvtri  30689  nmlno0  30814  nmlnoubi  30815  ubth  30892  hlipgt0  30933  ocnel  31317  elspansn2  31586  elspansn3  31591  normcan  31595  pjoml2  31630  lecm  31636  osum  31664  nmbdfnlb  32069  leopmul  32153  hstpyth  32248  cvnbtwn  32305  ssmd1  32330  ssmd2  32331  ssdmd1  32332  ssdmd2  32333  cvmd  32355  cvdmd  32356  superpos  32373  disji2f  32590  disjif  32591  disjif2  32594  preiman0  32719  padct  32731  ffs2  32739  bcm1n  32797  s2f1  32929  omndadd  33083  ogrpaddlt  33094  archiabl  33205  slmdlema  33209  lbslsat  33667  eulerpartlemb  34370  sgn3da  34544  fisshasheq  35120  cvmsdisj  35275  cvmlift2lem12  35319  satfrel  35372  satfrnmapom  35375  fmlasuc  35391  satffun  35414  satef  35421  sategoelfv  35425  lineintmo  36158  nn0prpwlem  36323  nn0prpw  36324  neibastop2lem  36361  lindsadd  37620  areacirc  37720  incsequz  37755  mettrifi  37764  ismtybnd  37814  heiborlem1  37818  rngoisocnv  37988  risci  37994  eqvrelqsel  38617  lfl1  39071  lkrlsp2  39104  omlfh3N  39260  cvrnbtwn  39272  cvrnbtwn2  39276  cvrnbtwn4  39280  cvlexch3  39333  cvlexch4N  39334  cvlatexchb1  39335  2llnne2N  39410  atcvrj0  39430  cvrat2  39431  ps-1  39479  3atlem5  39489  islln2a  39519  lplnriaN  39552  lplnribN  39553  llncvrlpln2  39559  lplncvrlvol2  39617  psubatN  39757  pmapglb2N  39773  pmapglb2xN  39774  2llnma1b  39788  paddasslem17  39838  pmod2iN  39851  pmodl42N  39853  hlmod1i  39858  atmod1i1  39859  atmod1i2  39861  llnmod1i2  39862  pclcmpatN  39903  osumcllem8N  39965  pexmidlem3N  39974  pl42lem4N  39984  4atexlem7  40077  ltrnnid  40138  cdlemc4  40196  cdleme32a  40443  cdlemeg46gfre  40534  cdlemf2  40564  cdlemg4c  40614  trlcoat  40725  tendovalco  40767  tendoeq2  40776  cdlemk36  40915  diael  41045  diatrl  41046  dicelval1stN  41190  dicelval2nd  41191  dihlspsnat  41335  dochkr1  41480  lcfrlem9  41552  mapdh8e  41786  hdmapval0  41835  hgmapval0  41894  nnadddir  42305  dvdsexpnn0  42369  incssnn0  42722  pell14qrexpcl  42878  pell14qrgap  42886  congadd  42978  acongsym  42988  acongtr  42990  dvdsacongtr  42996  jm2.19lem3  43003  jm2.19lem4  43004  jm2.26lem3  43013  onexlimgt  43255  nadd2rabex  43399  ismnushort  44320  bi13impia  44509  3impcombi  44837  ioogtlb  45508  iocgtlb  45515  iocleub  45516  icoltub  45521  iooltub  45523  limclner  45666  limsupre3lem  45747  climuzlem  45758  fsupdm  46857  finfdm  46861  elfzelfzlble  47333  subsubelfzo0  47338  m1modnep2mod  47354  iccpartigtl  47410  sqrtpwpw2p  47525  fmtnoprmfac1lem  47551  fmtno4prmfac  47559  evenltle  47704  even3prm2  47706  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem1  47792  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  uhgrimisgrgriclem  47898  isubgr3stgrlem7  47939  clnbgr3stgrgrlic  47979  upgrwlkupwlk  48056  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  lincscmcl  48349  lindslinindimp2lem4  48378  lincresunit2  48395  lincresunit3  48398  elfzolborelfzop1  48436  m1modmmod  48442  rege1logbzge0  48480  fllog2  48489  dignn0ldlem  48523  rrx2pnecoorneor  48636  rrx2plord2  48643  rrx2linest  48663  ipolub  48877  ipoglb  48880