Theorem 3impia 1116

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

This theorem is referenced by:  mopick2  2632  ceqsalt  3505  3gencl  3517  vtoclgft  3540  vtoclegft  3574  rspc6v  3631  mob2  3711  moi  3714  reupick3  4319  disjne  4454  elpr2elpr  4869  disji2  5130  disji  5131  tz7.2  5660  sofld  6186  ordintdif  6414  funopg  6582  fvun1  6982  fvopab6  7031  fveqressseq  7081  fvcofneq  7094  fprg  7155  2f1fvneq  7262  isores3  7335  ovmpt4g  7558  ovmpos  7559  ov2gf  7560  ofrval  7686  sorpssuni  7726  sorpssint  7727  poxp  8119  poseq  8149  suppss2  8191  frrlem12  8288  smoel  8366  smoord  8371  smogt  8373  oaass  8567  oewordi  8597  oeoalem  8602  oeoelem  8604  nnawordi  8627  nnaass  8628  naddssim  8690  qsel  8796  xpdom3  9076  onsdominel  9132  mapdom3  9155  sdomdomtrfi  9210  domsdomtrfi  9211  php  9216  onomeneq  9234  fisseneq  9263  cantnflem1  9690  ttrclss  9721  cfslbn  10268  cfsmolem  10271  cfcoflem  10273  infpssrlem4  10307  fin23lem7  10317  fin23lem25  10325  isf34lem7  10380  hsmexlem2  10428  axcc3  10439  axdc4lem  10456  tskss  10759  gruss  10797  gruurn  10799  gruiun  10800  gruel  10804  gruen  10813  grudomon  10818  grothac  10831  axpre-sup  11170  axsup  11296  addn0nid  11641  letrp1  12065  p1le  12066  lemul1a  12075  infrelb  12206  zextle  12642  zextlt  12643  btwnnz  12645  gtndiv  12646  uzind2  12662  fzind  12667  eluzsubOLD  12865  zsupss  12928  xrltne  13149  lemaxle  13181  qbtwnre  13185  qbtwnxr  13186  xlemul1a  13274  icogelb  13382  iccleub  13386  iccsplit  13469  uzsubsubfz  13530  elfz0fzfz0  13613  difelfznle  13622  fvffz0  13626  elfzo0le  13683  fzonmapblen  13685  fzofzim  13686  ceile  13821  modadd1  13880  muladdmodid  13883  modmul1  13896  modirr  13914  fsuppmapnn0fiub0  13965  expcl2lem  14046  expclzlem  14056  expnegz  14069  leexp2r  14146  bcval4  14274  bccmpl  14276  hashbnd  14303  hashunsnggt  14361  hashgt23el  14391  hashfundm  14409  elovmpowrd  14515  ccatval2  14535  ccatrcl1  14551  wrdl1s1  14571  ccat2s1fvw  14595  swrdsb0eq  14620  swrdccatin1  14682  pfxccatpfx2  14694  repswswrd  14741  cshwcsh2id  14786  absexpz  15259  climbdd  15625  iseraltlem2  15636  binomfallfac  15992  dvdsle  16260  divalgb  16354  ndvdssub  16359  dvdsgcd  16493  dfgcd2  16495  rplpwr  16506  lcmgcdlem  16550  lcmfunsn  16588  coprmdvds1  16596  qredeq  16601  2mulprm  16637  prmdvdsexpr  16661  nnnn0modprm0  16746  prm23ge5  16755  pcexp  16799  difsqpwdvds  16827  prmpwdvds  16844  ramcl  16969  cshwshashlem3  17038  cshwrepswhash1  17043  elrestr  17381  mreintcl  17546  mremre  17555  mrieqv2d  17590  initoeu2lem1  17974  funcestrcsetclem9  18110  funcsetcestrclem9  18125  prstr  18263  drsdirfi  18268  latnlej  18419  latnlej2  18422  acsdrsel  18506  acsdrscl  18509  mrelatglb  18523  mrelatlub  18525  isnmgm  18575  grpasscan1  18929  grpinvnz  18937  mulgneg2  19031  gsmsymgrfix  19344  f1omvdco2  19364  symggen  19386  odcl2  19481  odhash3  19492  lsmss1  19581  lsmss2  19583  efgred  19664  efgcpbl  19672  ablfacrp  19984  ablfac1eu  19991  ablfaclem3  20005  dvdsrmul1  20267  dvdsunit  20277  irredmul  20327  c0snmgmhm  20360  lmodlema  20707  psgnodpmr  21453  phlssphl  21522  lindsss  21689  lindfmm  21692  ply1scln0  22134  dmatelnd  22318  mdetdiaglem  22420  mdet0  22428  mdetunilem7  22440  slesolinv  22502  cramerimplem3  22507  cpmatpmat  22532  m2cpminvid2lem  22576  chfacfscmul0  22680  chfacfpmmul0  22684  riinopn  22730  clsndisj  22899  cnpf2  23074  hausnei2  23177  cmpcov  23213  cmpfii  23233  unconn  23253  t1connperf  23260  nrmr0reg  23573  fbfinnfr  23665  filuni  23709  alexsubALT  23875  tmdgsum  23919  cuspcvg  24126  mopni  24321  isngp4  24441  metdsre  24689  iimulcl  24780  phtpc01  24842  clmmulg  24948  cfilucfil4  25169  bcthlem5  25176  bcth  25177  bcth3  25179  itg1le  25563  itg2le  25589  bddmulibl  25688  bddiblnc  25691  dvnres  25781  cpnord  25785  dvnfre  25804  deg1ge  25954  dgr1term  26112  aaliou3lem2  26195  sincosq1lem  26347  cxpge0  26531  cxpmul2  26537  logrec  26609  logbgcd1irr  26640  sqfpc  26982  bcmono  27123  gausslemma2dlem1a  27211  gausslemma2dlem2  27213  gausslemma2dlem4  27215  2lgsoddprmlem3  27260  pntrmax  27410  qabvexp  27472  ostth2lem2  27480  nosepon  27511  nolesgn2o  27517  nogesgn1o  27519  nosepnelem  27525  nosepne  27526  nosepdmlem  27529  nosepdm  27530  nodenselem8  27537  noresle  27543  noetasuplem4  27582  noetainflem4  27586  scutbdaylt  27664  addsuniflem  27831  ssltmul1  27960  precsexlem6  28023  precsexlem7  28024  precsexlem11  28028  sltonold  28066  ax5seglem4  28623  axeuclidlem  28653  uhgredgrnv  28823  usgredg4  28907  nbuhgr2vtx1edgblem  29041  vtxduhgr0e  29168  vtxduhgr0nedg  29182  rusgrpropnb  29273  uspgr2wlkeqi  29338  redwlklem  29361  lfgrwlkprop  29377  2pthnloop  29421  spthonepeq  29442  pthdlem2lem  29457  crctcshwlkn0lem3  29499  crctcshwlkn0lem5  29501  crctcshwlkn0lem7  29503  crctcshwlkn0  29508  wlkiswwlks1  29554  wlkiswwlks2  29562  wlkiswwlksupgr2  29564  wwlksnext  29580  wwlksnextproplem2  29597  wspthsnonn0vne  29604  2pthon3v  29630  rusgrnumwwlk  29662  erclwwlkeqlen  29705  erclwwlksym  29707  erclwwlktr  29708  erclwwlkneqlen  29754  erclwwlknsym  29756  erclwwlkntr  29757  uhgr3cyclex  29868  upgreupthseg  29895  eupth2lem3lem4  29917  eucrctshift  29929  4cycl2vnunb  29976  nvs  30349  nvtri  30356  nmlno0  30481  nmlnoubi  30482  ubth  30559  hlipgt0  30600  ocnel  30984  elspansn2  31253  elspansn3  31258  normcan  31262  pjoml2  31297  lecm  31303  osum  31331  nmbdfnlb  31736  leopmul  31820  hstpyth  31915  cvnbtwn  31972  ssmd1  31997  ssmd2  31998  ssdmd1  31999  ssdmd2  32000  cvmd  32022  cvdmd  32023  superpos  32040  disji2f  32241  disjif  32242  disjif2  32245  preiman0  32364  padct  32377  ffs2  32386  bcm1n  32439  s2f1  32544  omndadd  32660  ogrpaddlt  32671  archiabl  32780  slmdlema  32784  lbslsat  33155  eulerpartlemb  33831  sgn3da  34004  fisshasheq  34568  cvmsdisj  34725  cvmlift2lem12  34769  satfrel  34822  satfrnmapom  34825  fmlasuc  34841  satffun  34864  satef  34871  sategoelfv  34875  lineintmo  35599  nn0prpwlem  35671  nn0prpw  35672  neibastop2lem  35709  lindsadd  36945  areacirc  37045  incsequz  37080  mettrifi  37089  ismtybnd  37139  heiborlem1  37143  rngoisocnv  37313  risci  37319  eqvrelqsel  37950  lfl1  38404  lkrlsp2  38437  omlfh3N  38593  cvrnbtwn  38605  cvrnbtwn2  38609  cvrnbtwn4  38613  cvlexch3  38666  cvlexch4N  38667  cvlatexchb1  38668  2llnne2N  38743  atcvrj0  38763  cvrat2  38764  ps-1  38812  3atlem5  38822  islln2a  38852  lplnriaN  38885  lplnribN  38886  llncvrlpln2  38892  lplncvrlvol2  38950  psubatN  39090  pmapglb2N  39106  pmapglb2xN  39107  2llnma1b  39121  paddasslem17  39171  pmod2iN  39184  pmodl42N  39186  hlmod1i  39191  atmod1i1  39192  atmod1i2  39194  llnmod1i2  39195  pclcmpatN  39236  osumcllem8N  39298  pexmidlem3N  39307  pl42lem4N  39317  4atexlem7  39410  ltrnnid  39471  cdlemc4  39529  cdleme32a  39776  cdlemeg46gfre  39867  cdlemf2  39897  cdlemg4c  39947  trlcoat  40058  tendovalco  40100  tendoeq2  40109  cdlemk36  40248  diael  40378  diatrl  40379  dicelval1stN  40523  dicelval2nd  40524  dihlspsnat  40668  dochkr1  40813  lcfrlem9  40885  mapdh8e  41119  hdmapval0  41168  hgmapval0  41227  nnadddir  41647  nn0rppwr  41687  nn0expgcd  41689  dvdsexpnn0  41695  incssnn0  41912  pell14qrexpcl  42068  pell14qrgap  42076  congadd  42168  acongsym  42178  acongtr  42180  dvdsacongtr  42186  jm2.19lem3  42193  jm2.19lem4  42194  jm2.26lem3  42203  onexlimgt  42455  nadd2rabex  42599  ismnushort  43523  bi13impia  43712  3impcombi  44041  ioogtlb  44667  iocgtlb  44674  iocleub  44675  icoltub  44680  iooltub  44682  limclner  44826  limsupre3lem  44907  climuzlem  44918  fsupdm  46017  finfdm  46021  elfzelfzlble  46488  subsubelfzo0  46493  iccpartigtl  46550  sqrtpwpw2p  46665  fmtnoprmfac1lem  46691  fmtno4prmfac  46699  evenltle  46844  even3prm2  46846  wtgoldbnnsum4prm  46929  bgoldbnnsum3prm  46931  bgoldbtbndlem1  46932  bgoldbtbndlem3  46934  bgoldbtbndlem4  46935  bgoldbtbnd  46936  upgrwlkupwlk  46977  funcringcsetcALTV2lem9  47135  funcringcsetclem9ALTV  47158  lincscmcl  47275  lindslinindimp2lem4  47304  lincresunit2  47321  lincresunit3  47324  elfzolborelfzop1  47362  m1modmmod  47369  rege1logbzge0  47407  fllog2  47416  dignn0ldlem  47450  rrx2pnecoorneor  47563  rrx2plord2  47570  rrx2linest  47590  ipolub  47775  ipoglb  47778