Theorem 3impia 1117

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 1116	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mopick2  2630  ceqsalt  3481  3gencl  3491  vtoclgft  3518  vtoclegft  3554  rspc6v  3609  mob2  3686  moi  3689  reupick3  4293  disjne  4418  elpr2elpr  4833  disji2  5091  disji  5092  tz7.2  5621  sofld  6160  ordintdif  6383  funopg  6550  fvun1  6952  fvopab6  7002  fveqressseq  7051  fvcofneq  7065  fprg  7127  isores3  7310  ovmpt4g  7536  ovmpos  7537  ov2gf  7538  ofrval  7665  sorpssuni  7708  sorpssint  7709  poxp  8107  poseq  8137  suppss2  8179  frrlem12  8276  smoel  8329  smoord  8334  smogt  8336  oaass  8525  oewordi  8555  oeoalem  8560  oeoelem  8562  nnawordi  8585  nnaass  8586  naddssim  8649  qsel  8769  xpdom3  9039  onsdominel  9090  mapdom3  9113  sdomdomtrfi  9165  domsdomtrfi  9166  php  9171  onomeneq  9178  fisseneq  9204  fodomfir  9279  cantnflem1  9642  ttrclss  9673  cfslbn  10220  cfsmolem  10223  cfcoflem  10225  infpssrlem4  10259  fin23lem7  10269  fin23lem25  10277  isf34lem7  10332  hsmexlem2  10380  axcc3  10391  axdc4lem  10408  tskss  10711  gruss  10749  gruurn  10751  gruiun  10752  gruel  10756  gruen  10765  grudomon  10770  grothac  10783  axpre-sup  11122  axsup  11249  addn0nid  11598  letrp1  12026  p1le  12027  lemul1a  12036  infrelb  12168  zextle  12607  zextlt  12608  btwnnz  12610  gtndiv  12611  uzind2  12627  fzind  12632  eluzsubOLD  12829  zsupss  12896  xrltne  13123  lemaxle  13155  qbtwnre  13159  qbtwnxr  13160  xlemul1a  13248  icogelb  13357  iccleub  13362  iccsplit  13446  uzsubsubfz  13507  elfz0fzfz0  13594  difelfznle  13603  fvffz0  13607  elfzo0le  13664  fzonmapblen  13669  fzofzim  13670  ceile  13811  modadd1  13870  muladdmodid  13875  modmul1  13889  modirr  13907  fsuppmapnn0fiub0  13958  expcl2lem  14038  expclzlem  14048  expnegz  14061  leexp2r  14139  bcval4  14272  bccmpl  14274  hashbnd  14301  hashunsnggt  14359  hashgt23el  14389  hashfundm  14407  elovmpowrd  14523  ccatval2  14543  ccatrcl1  14559  wrdl1s1  14579  ccat2s1fvw  14603  swrdsb0eq  14628  swrdccatin1  14690  pfxccatpfx2  14702  repswswrd  14749  cshwcsh2id  14794  absexpz  15271  climbdd  15638  iseraltlem2  15649  binomfallfac  16007  dvdsle  16280  divalgb  16374  ndvdssub  16379  dvdsgcd  16514  dfgcd2  16516  rplpwr  16528  nn0rppwr  16531  nn0expgcd  16534  lcmgcdlem  16576  lcmfunsn  16614  coprmdvds1  16622  qredeq  16627  2mulprm  16663  prmdvdsexpr  16687  nnnn0modprm0  16777  prm23ge5  16786  pcexp  16830  difsqpwdvds  16858  prmpwdvds  16875  ramcl  17000  cshwshashlem3  17068  cshwrepswhash1  17073  elrestr  17391  mreintcl  17556  mremre  17565  mrieqv2d  17600  initoeu2lem1  17976  funcestrcsetclem9  18109  funcsetcestrclem9  18124  prstr  18260  drsdirfi  18266  latnlej  18415  latnlej2  18418  acsdrsel  18502  acsdrscl  18505  mrelatglb  18519  mrelatlub  18521  isnmgm  18571  grpasscan1  18933  grpinvnz  18942  mulgneg2  19040  gsmsymgrfix  19358  f1omvdco2  19378  symggen  19400  odcl2  19495  odhash3  19506  lsmss1  19595  lsmss2  19597  efgred  19678  efgcpbl  19686  ablfacrp  19998  ablfac1eu  20005  ablfaclem3  20019  dvdsrmul1  20278  dvdsunit  20288  irredmul  20338  c0snmgmhm  20371  lmodlema  20771  psgnodpmr  21499  phlssphl  21568  lindsss  21733  lindfmm  21736  ply1scln0  22178  dmatelnd  22383  mdetdiaglem  22485  mdet0  22493  mdetunilem7  22505  slesolinv  22567  cramerimplem3  22572  cpmatpmat  22597  m2cpminvid2lem  22641  chfacfscmul0  22745  chfacfpmmul0  22749  riinopn  22795  clsndisj  22962  cnpf2  23137  hausnei2  23240  cmpcov  23276  cmpfii  23296  unconn  23316  t1connperf  23323  nrmr0reg  23636  fbfinnfr  23728  filuni  23772  alexsubALT  23938  tmdgsum  23982  cuspcvg  24188  mopni  24380  isngp4  24500  metdsre  24742  iimulcl  24833  phtpc01  24895  clmmulg  25001  cfilucfil4  25221  bcthlem5  25228  bcth  25229  bcth3  25231  itg1le  25614  itg2le  25640  bddmulibl  25740  bddiblnc  25743  dvnres  25833  cpnord  25837  dvnfre  25856  deg1ge  26003  dgr1term  26165  aaliou3lem2  26251  sincosq1lem  26406  cxpge0  26592  cxpmul2  26598  logrec  26673  logbgcd1irr  26704  sqfpc  27047  bcmono  27188  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem4  27280  2lgsoddprmlem3  27325  pntrmax  27475  qabvexp  27537  ostth2lem2  27545  nosepon  27577  nolesgn2o  27583  nogesgn1o  27585  nosepnelem  27591  nosepne  27592  nosepdmlem  27595  nosepdm  27596  nodenselem8  27603  noresle  27609  noetasuplem4  27648  noetainflem4  27652  scutbdaylt  27730  addsuniflem  27908  ssltmul1  28050  precsexlem6  28114  precsexlem7  28115  precsexlem11  28119  sltonold  28162  onnolt  28167  n0sfincut  28246  expadds  28320  ax5seglem4  28859  axeuclidlem  28889  uhgredgrnv  29057  usgredg4  29144  nbuhgr2vtx1edgblem  29278  vtxduhgr0e  29406  vtxduhgr0nedg  29420  rusgrpropnb  29511  uspgr2wlkeqi  29576  redwlklem  29599  lfgrwlkprop  29615  2pthnloop  29661  spthonepeq  29682  pthdlem2lem  29697  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  crctcshwlkn0lem7  29746  crctcshwlkn0  29751  wlkiswwlks1  29797  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wwlksnext  29823  wwlksnextproplem2  29840  wspthsnonn0vne  29847  2pthon3v  29873  rusgrnumwwlk  29905  erclwwlkeqlen  29948  erclwwlksym  29950  erclwwlktr  29951  erclwwlkneqlen  29997  erclwwlknsym  29999  erclwwlkntr  30000  uhgr3cyclex  30111  upgreupthseg  30138  eupth2lem3lem4  30160  eucrctshift  30172  4cycl2vnunb  30219  nvs  30592  nvtri  30599  nmlno0  30724  nmlnoubi  30725  ubth  30802  hlipgt0  30843  ocnel  31227  elspansn2  31496  elspansn3  31501  normcan  31505  pjoml2  31540  lecm  31546  osum  31574  nmbdfnlb  31979  leopmul  32063  hstpyth  32158  cvnbtwn  32215  ssmd1  32240  ssmd2  32241  ssdmd1  32242  ssdmd2  32243  cvmd  32265  cvdmd  32266  superpos  32283  disji2f  32506  disjif  32507  disjif2  32510  preiman0  32633  padct  32643  ffs2  32651  bcm1n  32718  sgn3da  32759  s2f1  32866  omndadd  33020  ogrpaddlt  33031  archiabl  33152  slmdlema  33156  lbslsat  33612  eulerpartlemb  34359  fisshasheq  35102  cvmsdisj  35257  cvmlift2lem12  35301  satfrel  35354  satfrnmapom  35357  fmlasuc  35373  satffun  35396  satef  35403  sategoelfv  35407  lineintmo  36145  nn0prpwlem  36310  nn0prpw  36311  neibastop2lem  36348  lindsadd  37607  areacirc  37707  incsequz  37742  mettrifi  37751  ismtybnd  37801  heiborlem1  37805  rngoisocnv  37975  risci  37981  eqvrelqsel  38607  lfl1  39063  lkrlsp2  39096  omlfh3N  39252  cvrnbtwn  39264  cvrnbtwn2  39268  cvrnbtwn4  39272  cvlexch3  39325  cvlexch4N  39326  cvlatexchb1  39327  2llnne2N  39402  atcvrj0  39422  cvrat2  39423  ps-1  39471  3atlem5  39481  islln2a  39511  lplnriaN  39544  lplnribN  39545  llncvrlpln2  39551  lplncvrlvol2  39609  psubatN  39749  pmapglb2N  39765  pmapglb2xN  39766  2llnma1b  39780  paddasslem17  39830  pmod2iN  39843  pmodl42N  39845  hlmod1i  39850  atmod1i1  39851  atmod1i2  39853  llnmod1i2  39854  pclcmpatN  39895  osumcllem8N  39957  pexmidlem3N  39966  pl42lem4N  39976  4atexlem7  40069  ltrnnid  40130  cdlemc4  40188  cdleme32a  40435  cdlemeg46gfre  40526  cdlemf2  40556  cdlemg4c  40606  trlcoat  40717  tendovalco  40759  tendoeq2  40768  cdlemk36  40907  diael  41037  diatrl  41038  dicelval1stN  41182  dicelval2nd  41183  dihlspsnat  41327  dochkr1  41472  lcfrlem9  41544  mapdh8e  41778  hdmapval0  41827  hgmapval0  41886  nnadddir  42258  dvdsexpnn0  42322  incssnn0  42699  pell14qrexpcl  42855  pell14qrgap  42863  congadd  42955  acongsym  42965  acongtr  42967  dvdsacongtr  42973  jm2.19lem3  42980  jm2.19lem4  42981  jm2.26lem3  42990  onexlimgt  43232  nadd2rabex  43375  ismnushort  44290  bi13impia  44479  3impcombi  44806  ioogtlb  45493  iocgtlb  45500  iocleub  45501  icoltub  45506  iooltub  45508  limclner  45649  limsupre3lem  45730  climuzlem  45741  fsupdm  46840  finfdm  46844  elfzelfzlble  47322  subsubelfzo0  47327  m1modnep2mod  47353  m1modmmod  47359  modlt0b  47364  mod2addne  47365  iccpartigtl  47424  sqrtpwpw2p  47539  fmtnoprmfac1lem  47565  fmtno4prmfac  47573  evenltle  47718  even3prm2  47720  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem1  47806  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  uhgrimisgrgriclem  47930  isubgr3stgrlem7  47971  clnbgr3stgrgrlic  48011  gpgedg2iv  48058  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  upgrwlkupwlk  48128  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  lincscmcl  48421  lindslinindimp2lem4  48450  lincresunit2  48467  lincresunit3  48470  elfzolborelfzop1  48508  rege1logbzge0  48548  fllog2  48557  dignn0ldlem  48591  rrx2pnecoorneor  48704  rrx2plord2  48711  rrx2linest  48731  ipolub  48976  ipoglb  48979