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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  mopick2  2665  ceqsalt  3488  3gencl  3498  vtoclgft  3520  rspc6v  3602  mob2  3678  moi  3681  reupick3  4283  disjne  4415  elpr2elpr  4834  disji2  5093  disji  5094  tz7.2  5644  sofld  6185  ordintdif  6412  funopg  6570  fvun1  6972  fvopab6  7024  fveqressseq  7074  fvcofneq  7088  fprg  7152  isores3  7333  ovmpt4g  7557  ovmpos  7558  ov2gf  7559  ofrval  7686  sorpssuni  7729  sorpssint  7730  poxp  8120  poseq  8150  suppss2  8192  frrlem12  8290  smoel  8343  smoord  8348  smogt  8350  oaass  8542  oewordi  8573  oeoalem  8578  oeoelem  8580  nnawordi  8603  nnaass  8604  naddssim  8668  qsel  8790  xpdom3  9059  onsdominel  9110  mapdom3  9133  sdomdomtrfi  9181  domsdomtrfi  9182  php  9187  onomeneq  9194  fisseneq  9219  fodomfir  9283  cantnflem1  9654  ttrclss  9685  cfslbn  10246  cfsmolem  10249  cfcoflem  10251  infpssrlem4  10285  fin23lem7  10295  fin23lem25  10303  isf34lem7  10358  hsmexlem2  10406  axcc3  10417  axdc4lem  10434  tskss  10738  gruss  10776  gruurn  10778  gruiun  10779  gruel  10783  gruen  10792  grudomon  10797  grothac  10810  axpre-sup  11149  axsup  11280  addn0nid  11629  letrp1  12054  p1le  12055  lemul1a  12064  infrelb  12195  nnadddir  12287  zextle  12664  zextlt  12665  btwnnz  12667  gtndiv  12668  uzind2  12684  fzind  12689  zsupss  12956  xrltne  13183  lemaxle  13216  qbtwnre  13220  qbtwnxr  13221  xlemul1a  13309  icogelb  13418  iccleub  13423  iccsplit  13507  uzsubsubfz  13570  elfz0fzfz0  13657  difelfznle  13666  fvffz0  13670  elfzo0le  13728  fzonmapblen  13733  fzofzim  13734  ceile  13878  modadd1  13937  muladdmodid  13942  modmul1  13956  modirr  13974  fsuppmapnn0fiub0  14025  expcl2lem  14105  expclzlem  14115  expnegz  14128  leexp2r  14206  bcval4  14339  bccmpl  14341  hashbnd  14368  hashunsnggt  14426  hashgt23el  14457  hashfundm  14475  elovmpowrd  14591  ccatval2  14611  ccatrcl1  14628  wrdl1s1  14648  ccat2s1fvw  14672  swrdsb0eq  14697  swrdccatin1  14758  pfxccatpfx2  14770  repswswrd  14817  cshwcsh2id  14861  sgn3da  15134  absexpz  15352  climbdd  15719  iseraltlem2  15730  binomfallfac  16090  dvdsle  16363  divalgb  16457  ndvdssub  16462  dvdsgcd  16597  dfgcd2  16599  rplpwr  16611  nn0rppwr  16614  nn0expgcd  16617  lcmgcdlem  16659  lcmfunsn  16697  coprmdvds1  16705  qredeq  16710  2mulprm  16746  prmdvdsexpr  16771  nnnn0modprm0  16861  prm23ge5  16870  pcexp  16914  difsqpwdvds  16942  prmpwdvds  16959  ramcl  17084  cshwshashlem3  17152  cshwrepswhash1  17157  elrestr  17476  mreintcl  17642  mremre  17651  mrieqv2d  17690  initoeu2lem1  18066  funcestrcsetclem9  18199  funcsetcestrclem9  18214  prstr  18350  drsdirfi  18356  latnlej  18507  latnlej2  18510  acsdrsel  18594  acsdrscl  18597  mrelatglb  18611  mrelatlub  18613  isnmgm  18697  grpasscan1  19063  grpinvnz  19071  mulgneg2  19169  gsmsymgrfix  19493  f1omvdco2  19513  symggen  19535  odcl2  19630  odhash3  19641  lsmss1  19730  lsmss2  19732  efgred  19813  efgcpbl  19821  ablfacrp  20133  ablfac1eu  20140  ablfaclem3  20154  omndadd  20193  ogrpaddlt  20203  dvdsrmul1  20447  dvdsunit  20457  irredmul  20507  c0snmgmhm  20540  lmodlema  20986  psgnodpmr  21740  phlssphl  21809  lindsss  21974  lindfmm  21977  ply1scln0  22452  dmatelnd  22653  mdetdiaglem  22755  mdet0  22763  mdetunilem7  22775  slesolinv  22837  cramerimplem3  22842  cpmatpmat  22867  m2cpminvid2lem  22911  chfacfscmul0  23015  chfacfpmmul0  23019  riinopn  23065  clsndisj  23232  cnpf2  23407  hausnei2  23510  cmpcov  23546  cmpfii  23566  unconn  23586  t1connperf  23593  nrmr0reg  23906  fbfinnfr  23998  filuni  24042  alexsubALT  24208  tmdgsum  24252  cuspcvg  24457  mopni  24649  isngp4  24769  metdsre  25011  iimulcl  25096  phtpc01  25155  clmmulg  25260  cfilucfil4  25480  bcthlem5  25487  bcth  25488  bcth3  25490  itg1le  25872  itg2le  25898  bddmulibl  25998  bddiblnc  26001  dvnres  26090  cpnord  26094  dvnfre  26111  deg1ge  26255  dgr1term  26417  aaliou3lem2  26506  sincosq1lem  26662  cxpge0  26848  cxpmul2  26854  logrec  26928  logbgcd1irr  26959  sqfpc  27301  bcmono  27441  gausslemma2dlem1a  27529  gausslemma2dlem2  27531  gausslemma2dlem4  27533  2lgsoddprmlem3  27578  pntrmax  27728  qabvexp  27790  ostth2lem2  27798  nosepon  27829  nolesgn2o  27835  nogesgn1o  27837  nosepnelem  27843  nosepne  27844  nosepdmlem  27847  nosepdm  27848  nodenselem8  27855  noresle  27861  noetasuplem4  27900  noetainflem4  27904  cutbdaylt  27991  eqcuts3  27997  addsuniflem  28194  sltmuls1  28340  precsexlem6  28405  precsexlem7  28406  precsexlem11  28410  ltonold  28454  onnolt  28459  n0fincut  28548  oldfib  28570  expadds  28628  ax5seglem4  29282  axeuclidlem  29312  uhgredgrnv  29480  usgredg4  29567  nbuhgr2vtx1edgblem  29701  vtxduhgr0e  29828  vtxduhgr0nedg  29842  rusgrpropnb  29933  uspgr2wlkeqi  29997  redwlklem  30019  lfgrwlkprop  30035  2pthnloop  30080  spthonepeq  30101  pthdlem2lem  30116  crctcshwlkn0lem3  30161  crctcshwlkn0lem5  30163  crctcshwlkn0lem7  30165  crctcshwlkn0  30170  wlkiswwlks1  30216  wlkiswwlks2  30224  wlkiswwlksupgr2  30226  wwlksnext  30242  wwlksnextproplem2  30259  wspthsnonn0vne  30266  2pthon3v  30292  rusgrnumwwlk  30327  erclwwlkeqlen  30370  erclwwlksym  30372  erclwwlktr  30373  erclwwlkneqlen  30419  erclwwlknsym  30421  erclwwlkntr  30422  uhgr3cyclex  30533  upgreupthseg  30560  eupth2lem3lem4  30582  eucrctshift  30594  4cycl2vnunb  30641  nvs  31015  nvtri  31022  nmlno0  31147  nmlnoubi  31148  ubth  31225  hlipgt0  31266  ocnel  31650  elspansn2  31919  elspansn3  31924  normcan  31928  pjoml2  31963  lecm  31969  osum  31997  nmbdfnlb  32402  leopmul  32486  hstpyth  32581  cvnbtwn  32638  ssmd1  32663  ssmd2  32664  ssdmd1  32665  ssdmd2  32666  cvmd  32688  cvdmd  32689  superpos  32706  disji2f  32922  disjif  32923  disjif2  32926  preiman0  33055  padct  33063  ffs2  33072  bcm1n  33140  s2f1  33265  archiabl  33518  slmdlema  33523  lbslsat  34006  eulerpartlemb  34758  nelscottrankgt  35518  fisshasheq  35606  cvmsdisj  35762  cvmlift2lem12  35806  satfrel  35859  satfrnmapom  35862  fmlasuc  35878  satffun  35901  satef  35908  sategoelfv  35912  lineintmo  36649  nmuladdss  36690  nn0prpwlem  36833  nn0prpw  36834  neibastop2lem  36871  tr0elw  36995  lindsadd  38264  areacirc  38364  incsequz  38399  mettrifi  38408  ismtybnd  38458  heiborlem1  38462  rngoisocnv  38632  risci  38638  eqvrelqsel  39349  lfl1  39844  lkrlsp2  39877  omlfh3N  40033  cvrnbtwn  40045  cvrnbtwn2  40049  cvrnbtwn4  40053  cvlexch3  40106  cvlexch4N  40107  cvlatexchb1  40108  2llnne2N  40182  atcvrj0  40202  cvrat2  40203  ps-1  40251  3atlem5  40261  islln2a  40291  lplnriaN  40324  lplnribN  40325  llncvrlpln2  40331  lplncvrlvol2  40389  psubatN  40529  pmapglb2N  40545  pmapglb2xN  40546  2llnma1b  40560  paddasslem17  40610  pmod2iN  40623  pmodl42N  40625  hlmod1i  40630  atmod1i1  40631  atmod1i2  40633  llnmod1i2  40634  pclcmpatN  40675  osumcllem8N  40737  pexmidlem3N  40746  pl42lem4N  40756  4atexlem7  40849  ltrnnid  40910  cdlemc4  40968  cdleme32a  41215  cdlemeg46gfre  41306  cdlemf2  41336  cdlemg4c  41386  trlcoat  41497  tendovalco  41539  tendoeq2  41548  cdlemk36  41687  diael  41817  diatrl  41818  dicelval1stN  41962  dicelval2nd  41963  dihlspsnat  42107  dochkr1  42252  lcfrlem9  42324  mapdh8e  42558  hdmapval0  42607  hgmapval0  42666  dvdsexpnn0  43095  incssnn0  43442  pell14qrexpcl  43594  pell14qrgap  43602  congadd  43693  acongsym  43703  acongtr  43705  dvdsacongtr  43711  jm2.19lem3  43718  jm2.19lem4  43719  jm2.26lem3  43728  onexlimgt  43970  nadd2rabex  44113  ismnushort  45011  bi13impia  45198  3impcombi  45525  ioogtlb  46211  iocgtlb  46218  iocleub  46219  icoltub  46224  iooltub  46226  limclner  46365  limsupre3lem  46446  climuzlem  46457  fsupdm  47556  finfdm  47560  elfzelfzlble  48058  subsubelfzo0  48064  m1modnep2mod  48095  m1modmmod  48101  modlt0b  48106  mod2addne  48107  iccpartigtl  48172  sqrtpwpw2p  48290  fmtnoprmfac1lem  48316  fmtno4prmfac  48324  evenltle  48482  even3prm2  48484  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  bgoldbtbndlem1  48570  bgoldbtbndlem3  48572  bgoldbtbndlem4  48573  bgoldbtbnd  48574  uhgrimisgrgriclem  48695  isubgr3stgrlem7  48737  clnbgr3stgrgrlic  48785  gpgedg2iv  48832  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem6  48889  upgrwlkupwlk  48905  funcringcsetcALTV2lem9  49063  funcringcsetclem9ALTV  49086  lincscmcl  49212  lindslinindimp2lem4  49241  lincresunit2  49258  lincresunit3  49261  elfzolborelfzop1  49299  rege1logbzge0  49339  fllog2  49348  dignn0ldlem  49382  rrx2pnecoorneor  49495  rrx2plord2  49502  rrx2linest  49522  ipolub  49766  ipoglb  49769