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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 397  df-3an 1088

This theorem is referenced by:  mopick2  2641  3gencl  3472  vtoclgft  3491  mob2  3654  moi  3657  reupick3  4259  disjne  4394  elpr2elpr  4805  disji2  5061  disji  5062  tz7.2  5574  sofld  6089  ordintdif  6314  funopg  6466  fvun1  6856  fvopab6  6905  fveqressseq  6954  fvcofneq  6966  fprg  7024  2f1fvneq  7130  isores3  7202  ovmpt4g  7414  ovmpos  7415  ov2gf  7416  ofrval  7539  sorpssuni  7579  sorpssint  7580  poxp  7960  suppss2  8007  frrlem12  8104  smoel  8182  smoord  8187  smogt  8189  oaass  8377  oewordi  8407  oeoalem  8412  oeoelem  8414  nnawordi  8437  nnaass  8438  qsel  8568  xpdom3  8839  onsdominel  8895  mapdom3  8918  sdomdomtrfi  8969  domsdomtrfi  8970  php  8974  fisseneq  9012  cantnflem1  9425  ttrclss  9456  cfslbn  10024  cfsmolem  10027  cfcoflem  10029  infpssrlem4  10063  fin23lem7  10073  fin23lem25  10081  isf34lem7  10136  hsmexlem2  10184  axcc3  10195  axdc4lem  10212  tskss  10515  gruss  10553  gruurn  10555  gruiun  10556  gruel  10560  gruen  10569  grudomon  10574  grothac  10587  axpre-sup  10926  axsup  11051  addn0nid  11395  letrp1  11819  p1le  11820  lemul1a  11829  infrelb  11960  zextle  12393  zextlt  12394  btwnnz  12396  gtndiv  12397  uzind2  12413  fzind  12418  eluzsub  12613  zsupss  12676  xrltne  12896  lemaxle  12928  qbtwnre  12932  qbtwnxr  12933  xlemul1a  13021  icogelb  13129  iccleub  13133  iccsplit  13216  uzsubsubfz  13277  elfz0fzfz0  13360  difelfznle  13369  fvffz0  13373  elfzo0le  13429  fzonmapblen  13431  fzofzim  13432  ceile  13567  modadd1  13626  muladdmodid  13629  modmul1  13642  modirr  13660  fsuppmapnn0fiub0  13711  expcl2lem  13792  expclzlem  13804  expnegz  13815  leexp2r  13890  bcval4  14019  bccmpl  14021  hashbnd  14048  hashunsnggt  14107  hashgt23el  14137  elovmpowrd  14259  ccatval2  14281  ccatrcl1  14297  wrdl1s1  14317  ccat2s1fvw  14347  ccat2s1fvwOLD  14348  swrdsb0eq  14374  swrdccatin1  14436  pfxccatpfx2  14448  repswswrd  14495  cshwcsh2id  14539  absexpz  15015  climbdd  15381  iseraltlem2  15392  binomfallfac  15749  dvdsle  16017  divalgb  16111  ndvdssub  16116  dvdsgcd  16250  dfgcd2  16252  rplpwr  16265  lcmgcdlem  16309  lcmfunsn  16347  coprmdvds1  16355  qredeq  16360  2mulprm  16396  prmdvdsexpr  16420  nnnn0modprm0  16505  prm23ge5  16514  pcexp  16558  difsqpwdvds  16586  prmpwdvds  16603  ramcl  16728  cshwshashlem3  16797  cshwrepswhash1  16802  elrestr  17137  mreintcl  17302  mremre  17311  mrieqv2d  17346  initoeu2lem1  17727  funcestrcsetclem9  17863  funcsetcestrclem9  17878  prstr  18016  drsdirfi  18021  latnlej  18172  latnlej2  18175  acsdrsel  18259  acsdrscl  18262  mrelatglb  18276  mrelatlub  18278  isnmgm  18328  grpasscan1  18636  grpinvnz  18644  mulgneg2  18735  gsmsymgrfix  19034  f1omvdco2  19054  symggen  19076  odcl2  19170  odhash3  19179  lsmss1  19269  lsmss2  19271  efgred  19352  efgcpbl  19360  ablfacrp  19667  ablfac1eu  19674  ablfaclem3  19688  dvdsrmul1  19893  dvdsunit  19903  irredmul  19949  lmodlema  20126  psgnodpmr  20793  phlssphl  20862  lindsss  21029  lindfmm  21032  ply1scln0  21460  dmatelnd  21643  mdetdiaglem  21745  mdet0  21753  mdetunilem7  21765  slesolinv  21827  cramerimplem3  21832  cpmatpmat  21857  m2cpminvid2lem  21901  chfacfscmul0  22005  chfacfpmmul0  22009  riinopn  22055  clsndisj  22224  cnpf2  22399  hausnei2  22502  cmpcov  22538  cmpfii  22558  unconn  22578  t1connperf  22585  nrmr0reg  22898  fbfinnfr  22990  filuni  23034  alexsubALT  23200  tmdgsum  23244  cuspcvg  23451  mopni  23646  isngp4  23766  metdsre  24014  iimulcl  24098  phtpc01  24157  clmmulg  24262  cfilucfil4  24483  bcthlem5  24490  bcth  24491  bcth3  24493  itg1le  24876  itg2le  24902  bddmulibl  25001  bddiblnc  25004  dvnres  25093  cpnord  25097  dvnfre  25114  deg1ge  25261  dgr1term  25419  aaliou3lem2  25501  sincosq1lem  25652  cxpge0  25836  cxpmul2  25842  logrec  25911  logbgcd1irr  25942  sqfpc  26284  bcmono  26423  gausslemma2dlem1a  26511  gausslemma2dlem2  26513  gausslemma2dlem4  26515  2lgsoddprmlem3  26560  pntrmax  26710  qabvexp  26772  ostth2lem2  26780  ax5seglem4  27298  axeuclidlem  27328  uhgredgrnv  27498  usgredg4  27582  nbuhgr2vtx1edgblem  27716  vtxduhgr0e  27843  vtxduhgr0nedg  27857  rusgrpropnb  27948  uspgr2wlkeqi  28012  redwlklem  28036  lfgrwlkprop  28052  2pthnloop  28095  spthonepeq  28116  pthdlem2lem  28131  crctcshwlkn0lem3  28173  crctcshwlkn0lem5  28175  crctcshwlkn0lem7  28177  crctcshwlkn0  28182  wlkiswwlks1  28228  wlkiswwlks2  28236  wlkiswwlksupgr2  28238  wwlksnext  28254  wwlksnextproplem2  28271  wspthsnonn0vne  28278  2pthon3v  28304  rusgrnumwwlk  28336  erclwwlkeqlen  28379  erclwwlksym  28381  erclwwlktr  28382  erclwwlkneqlen  28428  erclwwlknsym  28430  erclwwlkntr  28431  uhgr3cyclex  28542  upgreupthseg  28569  eupth2lem3lem4  28591  eucrctshift  28603  4cycl2vnunb  28650  nvs  29021  nvtri  29028  nmlno0  29153  nmlnoubi  29154  ubth  29231  hlipgt0  29272  ocnel  29656  elspansn2  29925  elspansn3  29930  normcan  29934  pjoml2  29969  lecm  29975  osum  30003  nmbdfnlb  30408  leopmul  30492  hstpyth  30587  cvnbtwn  30644  ssmd1  30669  ssmd2  30670  ssdmd1  30671  ssdmd2  30672  cvmd  30694  cvdmd  30695  superpos  30712  disji2f  30912  disjif  30913  disjif2  30916  preiman0  31038  padct  31050  ffs2  31059  bcm1n  31112  s2f1  31215  omndadd  31328  ogrpaddlt  31339  archiabl  31448  slmdlema  31452  lbslsat  31695  eulerpartlemb  32331  sgn3da  32504  fisshasheq  33069  hashfundm  33070  cvmsdisj  33228  cvmlift2lem12  33272  satfrel  33325  satfrnmapom  33328  fmlasuc  33344  satffun  33367  satef  33374  sategoelfv  33378  poseq  33798  naddssim  33833  nosepon  33864  nolesgn2o  33870  nogesgn1o  33872  nosepnelem  33878  nosepne  33879  nosepdmlem  33882  nosepdm  33883  nodenselem8  33890  noresle  33896  noetasuplem4  33935  noetainflem4  33939  scutbdaylt  34008  lineintmo  34455  nn0prpwlem  34507  nn0prpw  34508  neibastop2lem  34545  lindsadd  35766  areacirc  35866  incsequz  35902  mettrifi  35911  ismtybnd  35961  heiborlem1  35965  rngoisocnv  36135  risci  36141  eqvrelqsel  36725  lfl1  37080  lkrlsp2  37113  omlfh3N  37269  cvrnbtwn  37281  cvrnbtwn2  37285  cvrnbtwn4  37289  cvlexch3  37342  cvlexch4N  37343  cvlatexchb1  37344  2llnne2N  37418  atcvrj0  37438  cvrat2  37439  ps-1  37487  3atlem5  37497  islln2a  37527  lplnriaN  37560  lplnribN  37561  llncvrlpln2  37567  lplncvrlvol2  37625  psubatN  37765  pmapglb2N  37781  pmapglb2xN  37782  2llnma1b  37796  paddasslem17  37846  pmod2iN  37859  pmodl42N  37861  hlmod1i  37866  atmod1i1  37867  atmod1i2  37869  llnmod1i2  37870  pclcmpatN  37911  osumcllem8N  37973  pexmidlem3N  37982  pl42lem4N  37992  4atexlem7  38085  ltrnnid  38146  cdlemc4  38204  cdleme32a  38451  cdlemeg46gfre  38542  cdlemf2  38572  cdlemg4c  38622  trlcoat  38733  tendovalco  38775  tendoeq2  38784  cdlemk36  38923  diael  39053  diatrl  39054  dicelval1stN  39198  dicelval2nd  39199  dihlspsnat  39343  dochkr1  39488  lcfrlem9  39560  mapdh8e  39794  hdmapval0  39843  hgmapval0  39902  nnadddir  40297  nn0rppwr  40330  nn0expgcd  40332  dvdsexpnn0  40338  incssnn0  40530  pell14qrexpcl  40686  pell14qrgap  40694  congadd  40785  acongsym  40795  acongtr  40797  dvdsacongtr  40803  jm2.19lem3  40810  jm2.19lem4  40811  jm2.26lem3  40820  ismnushort  41889  bi13impia  42078  3impcombi  42407  ioogtlb  43004  iocgtlb  43011  iocleub  43012  icoltub  43017  iooltub  43019  limclner  43163  limsupre3lem  43244  climuzlem  43255  elfzelfzlble  44782  subsubelfzo0  44787  iccpartigtl  44844  sqrtpwpw2p  44959  fmtnoprmfac1lem  44985  fmtno4prmfac  44993  evenltle  45138  even3prm2  45140  wtgoldbnnsum4prm  45223  bgoldbnnsum3prm  45225  bgoldbtbndlem1  45226  bgoldbtbndlem3  45228  bgoldbtbndlem4  45229  bgoldbtbnd  45230  upgrwlkupwlk  45271  c0snmgmhm  45441  funcringcsetcALTV2lem9  45571  funcringcsetclem9ALTV  45594  lincscmcl  45742  lindslinindimp2lem4  45771  lincresunit2  45788  lincresunit3  45791  elfzolborelfzop1  45829  m1modmmod  45836  rege1logbzge0  45874  fllog2  45883  dignn0ldlem  45917  rrx2pnecoorneor  46030  rrx2plord2  46037  rrx2linest  46057  ipolub  46243  ipoglb  46246