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  2662  ceqsalt  3483  3gencl  3493  vtoclgft  3515  rspc6v  3597  mob2  3673  moi  3676  reupick3  4276  disjne  4408  elpr2elpr  4829  disji2  5087  disji  5088  tz7.2  5638  sofld  6180  ordintdif  6409  funopg  6567  fvun1  6969  fvopab6  7021  fveqressseq  7072  fvcofneq  7086  fprg  7152  isores3  7336  ovmpt4g  7560  ovmpos  7561  ov2gf  7562  ofrval  7690  sorpssuni  7733  sorpssint  7734  poxp  8126  poseq  8156  suppss2  8198  frrlem12  8296  smoel  8349  smoord  8354  smogt  8356  oaass  8548  oewordi  8579  oeoalem  8584  oeoelem  8586  nnawordi  8609  nnaass  8610  naddssim  8674  qsel  8796  xpdom3  9073  onsdominel  9124  mapdom3  9147  sdomdomtrfi  9195  domsdomtrfi  9196  php  9201  onomeneq  9208  fisseneq  9233  fodomfir  9297  cantnflem1  9668  ttrclss  9699  cfslbn  10269  cfsmolem  10272  cfcoflem  10274  infpssrlem4  10308  fin23lem7  10318  fin23lem25  10326  isf34lem7  10381  hsmexlem2  10429  axcc3  10440  axdc4lem  10457  tskss  10767  gruss  10805  gruurn  10807  gruiun  10808  gruel  10812  gruen  10821  grudomon  10826  grothac  10839  axpre-sup  11178  axsup  11309  addn0nid  11658  letrp1  12083  p1le  12084  lemul1a  12093  infrelb  12224  nnadddir  12316  zextle  12694  zextlt  12695  btwnnz  12697  gtndiv  12698  uzind2  12714  fzind  12719  zsupss  12986  xrltne  13214  lemaxle  13247  qbtwnre  13251  qbtwnxr  13252  xlemul1a  13340  icogelb  13449  iccleub  13454  iccsplit  13538  uzsubsubfz  13601  elfz0fzfz0  13688  difelfznle  13697  fvffz0  13701  elfzo0le  13759  fzonmapblen  13764  fzofzim  13765  ceile  13910  modadd1  13969  muladdmodid  13974  modmul1  13988  modirr  14006  fsuppmapnn0fiub0  14057  expcl2lem  14137  expclzlem  14147  expnegz  14160  leexp2r  14238  bcval4  14371  bccmpl  14373  hashbnd  14400  hashunsnggt  14458  hashgt23el  14489  hashfundm  14507  elovmpowrd  14623  ccatval2  14643  ccatrcl1  14661  wrdl1s1  14682  ccat2s1fvw  14706  swrdsb0eq  14733  swrdccatin1  14794  pfxccatpfx2  14806  repswswrd  14855  cshwcsh2id  14899  sgn3da  15174  absexpz  15392  climbdd  15759  iseraltlem2  15770  binomfallfac  16127  dvdsle  16400  divalgb  16494  ndvdssub  16499  dvdsgcd  16634  dfgcd2  16636  rplpwr  16648  nn0rppwr  16651  nn0expgcd  16654  lcmgcdlem  16696  lcmfunsn  16734  coprmdvds1  16742  qredeq  16747  2mulprm  16783  prmdvdsexpr  16808  nnnn0modprm0  16898  prm23ge5  16907  pcexp  16951  difsqpwdvds  16979  prmpwdvds  16996  ramcl  17121  cshwshashlem3  17189  cshwrepswhash1  17194  elrestr  17513  mreintcl  17679  mremre  17688  mrieqv2d  17727  initoeu2lem1  18103  funcestrcsetclem9  18236  funcsetcestrclem9  18251  prstr  18387  drsdirfi  18393  latnlej  18544  latnlej2  18547  acsdrsel  18631  acsdrscl  18634  mrelatglb  18648  mrelatlub  18650  isnmgm  18734  grpasscan1  19125  grpinvnz  19133  mulgneg2  19231  gsmsymgrfix  19555  f1omvdco2  19575  symggen  19597  odcl2  19692  odhash3  19703  lsmss1  19792  lsmss2  19794  efgred  19875  efgcpbl  19883  ablfacrp  20195  ablfac1eu  20202  ablfaclem3  20216  omndadd  20255  ogrpaddlt  20265  dvdsrmul1  20510  dvdsunit  20520  irredmul  20570  c0snmgmhm  20603  lmodlema  21049  psgnodpmr  21803  phlssphl  21872  lindsss  22037  lindfmm  22040  ply1scln0  22517  dmatelnd  22718  mdetdiaglem  22820  mdet0  22828  mdetunilem7  22840  slesolinv  22905  cramerimplem3  22910  cpmatpmat  22935  m2cpminvid2lem  22979  chfacfscmul0  23083  chfacfpmmul0  23087  riinopn  23133  clsndisj  23300  cnpf2  23475  hausnei2  23578  cmpcov  23614  cmpfii  23634  unconn  23654  t1connperf  23661  nrmr0reg  23975  fbfinnfr  24067  filuni  24111  alexsubALT  24277  tmdgsum  24321  cuspcvg  24526  mopni  24718  isngp4  24838  metdsre  25080  iimulcl  25165  phtpc01  25224  clmmulg  25329  cfilucfil4  25549  bcthlem5  25556  bcth  25557  bcth3  25559  itg1le  25941  itg2le  25967  bddmulibl  26066  bddiblnc  26069  dvnres  26158  cpnord  26162  dvnfre  26179  deg1ge  26323  dgr1term  26486  aaliou3lem2  26579  sincosq1lem  26735  cxpge0  26920  cxpmul2  26926  logrec  27000  logbgcd1irr  27031  sqfpc  27373  bcmono  27513  gausslemma2dlem1a  27601  gausslemma2dlem2  27603  gausslemma2dlem4  27605  2lgsoddprmlem3  27650  pntrmax  27800  qabvexp  27862  ostth2lem2  27870  nosepon  27901  nolesgn2o  27907  nogesgn1o  27909  nosepnelem  27915  nosepne  27916  nosepdmlem  27919  nosepdm  27920  nodenselem8  27927  noresle  27933  noetasuplem4  27972  noetainflem4  27976  cutbdaylt  28063  eqcuts3  28069  addsuniflem  28266  sltmuls1  28412  precsexlem6  28477  precsexlem7  28478  precsexlem11  28482  ltonold  28526  onnolt  28531  n0fincut  28620  oldfib  28642  expadds  28700  ax5seglem4  29389  axeuclidlem  29419  uhgredgrnv  29587  usgredg4  29677  nbuhgr2vtx1edgblem  29811  vtxduhgr0e  29938  vtxduhgr0nedg  29952  rusgrpropnb  30043  uspgr2wlkeqi  30107  redwlklem  30129  lfgrwlkprop  30149  2pthnloop  30196  spthonepeq  30217  pthdlem2lem  30232  crctcshwlkn0lem3  30280  crctcshwlkn0lem5  30282  crctcshwlkn0lem7  30284  crctcshwlkn0  30289  wlkiswwlks1  30335  wlkiswwlks2  30343  wlkiswwlksupgr2  30345  wwlksnext  30361  wwlksnextproplem2  30378  wspthsnonn0vne  30385  2pthon3v  30411  rusgrnumwwlk  30446  erclwwlkeqlen  30489  erclwwlksym  30491  erclwwlktr  30492  erclwwlkneqlen  30538  erclwwlknsym  30540  erclwwlkntr  30541  uhgr3cyclex  30662  upgreupthseg  30689  eupth2lem3lem4  30711  eucrctshift  30723  4cycl2vnunb  30770  nvs  31144  nvtri  31151  nmlno0  31276  nmlnoubi  31277  ubth  31354  hlipgt0  31395  ocnel  31779  elspansn2  32048  elspansn3  32053  normcan  32057  pjoml2  32092  lecm  32098  osum  32126  nmbdfnlb  32531  leopmul  32615  hstpyth  32710  cvnbtwn  32767  ssmd1  32792  ssmd2  32793  ssdmd1  32794  ssdmd2  32795  cvmd  32817  cvdmd  32818  superpos  32835  disji2f  33050  disjif  33051  disjif2  33054  preiman0  33182  padct  33189  ffs2  33198  bcm1n  33266  s2f1  33389  archiabl  33638  slmdlema  33643  lbslsat  34126  eulerpartlemb  34879  nelscottrankgt  35632  fisshasheq  35717  cvmsdisj  35849  cvmlift2lem12  35893  satfrel  35946  satfrnmapom  35949  fmlasuc  35965  satffun  35988  satef  35995  sategoelfv  35999  lineintmo  36737  nmuladdss  36793  nn0prpwlem  36941  nn0prpw  36942  neibastop2lem  36979  tr0elw  37103  lindsadd  38367  areacirc  38462  incsequz  38498  mettrifi  38507  ismtybnd  38557  heiborlem1  38561  rngoisocnv  38731  risci  38737  eqvrelqsel  39448  lfl1  39943  lkrlsp2  39976  omlfh3N  40132  cvrnbtwn  40144  cvrnbtwn2  40148  cvrnbtwn4  40152  cvlexch3  40205  cvlexch4N  40206  cvlatexchb1  40207  2llnne2N  40281  atcvrj0  40301  cvrat2  40302  ps-1  40350  3atlem5  40360  islln2a  40390  lplnriaN  40423  lplnribN  40424  llncvrlpln2  40430  lplncvrlvol2  40488  psubatN  40628  pmapglb2N  40644  pmapglb2xN  40645  2llnma1b  40659  paddasslem17  40709  pmod2iN  40722  pmodl42N  40724  hlmod1i  40729  atmod1i1  40730  atmod1i2  40732  llnmod1i2  40733  pclcmpatN  40774  osumcllem8N  40836  pexmidlem3N  40845  pl42lem4N  40855  4atexlem7  40948  ltrnnid  41009  cdlemc4  41067  cdleme32a  41314  cdlemeg46gfre  41405  cdlemf2  41435  cdlemg4c  41485  trlcoat  41596  tendovalco  41638  tendoeq2  41647  cdlemk36  41786  diael  41916  diatrl  41917  dicelval1stN  42061  dicelval2nd  42062  dihlspsnat  42206  dochkr1  42351  lcfrlem9  42423  mapdh8e  42657  hdmapval0  42706  hgmapval0  42765  dvdsexpnn0  43209  incssnn0  43556  pell14qrexpcl  43708  pell14qrgap  43716  congadd  43807  acongsym  43817  acongtr  43819  dvdsacongtr  43825  jm2.19lem3  43832  jm2.19lem4  43833  jm2.26lem3  43842  onexlimgt  44084  nadd2rabex  44227  ismnushort  45125  bi13impia  45312  3impcombi  45639  ioogtlb  46325  iocgtlb  46332  iocleub  46333  icoltub  46338  iooltub  46340  limclner  46479  limsupre3lem  46560  climuzlem  46571  fsupdm  47670  finfdm  47674  elfzelfzlble  48209  subsubelfzo0  48215  m1modnep2mod  48246  m1modmmod  48252  modlt0b  48257  mod2addne  48258  iccpartigtl  48323  sqrtpwpw2p  48441  fmtnoprmfac1lem  48467  fmtno4prmfac  48475  evenltle  48633  even3prm2  48635  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  bgoldbtbndlem1  48721  bgoldbtbndlem3  48723  bgoldbtbndlem4  48724  bgoldbtbnd  48725  uhgrimisgrgriclem  48846  isubgr3stgrlem7  48888  clnbgr3stgrgrlic  48936  gpgedg2iv  48983  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  upgrwlkupwlk  49056  funcringcsetcALTV2lem9  49213  funcringcsetclem9ALTV  49236  lincscmcl  49362  lindslinindimp2lem4  49391  lincresunit2  49408  lincresunit3  49411  elfzolborelfzop1  49449  rege1logbzge0  49489  fllog2  49498  dignn0ldlem  49532  rrx2pnecoorneor  49645  rrx2plord2  49652  rrx2linest  49672  ipolub  49914  ipoglb  49917