Theorem 3impia 1123

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 1122	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  mopick2  2641  ceqsalt  3464  3gencl  3474  vtoclgft  3498  rspc6v  3581  mob2  3656  moi  3659  reupick3  4258  disjne  4383  elpr2elpr  4800  disji2  5056  disji  5057  tz7.2  5601  sofld  6138  ordintdif  6361  funopg  6519  fvun1  6918  fvopab6  6970  fveqressseq  7020  fvcofneq  7034  fprg  7098  isores3  7279  ovmpt4g  7503  ovmpos  7504  ov2gf  7505  ofrval  7632  sorpssuni  7675  sorpssint  7676  poxp  8068  poseq  8098  suppss2  8140  frrlem12  8237  smoel  8290  smoord  8295  smogt  8297  oaass  8486  oewordi  8517  oeoalem  8522  oeoelem  8524  nnawordi  8547  nnaass  8548  naddssim  8611  qsel  8733  xpdom3  9003  onsdominel  9054  mapdom3  9077  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  onomeneq  9138  fisseneq  9163  fodomfir  9228  cantnflem1  9601  ttrclss  9632  cfslbn  10180  cfsmolem  10183  cfcoflem  10185  infpssrlem4  10219  fin23lem7  10229  fin23lem25  10237  isf34lem7  10292  hsmexlem2  10340  axcc3  10351  axdc4lem  10368  tskss  10672  gruss  10710  gruurn  10712  gruiun  10713  gruel  10717  gruen  10726  grudomon  10731  grothac  10744  axpre-sup  11083  axsup  11212  addn0nid  11561  letrp1  11990  p1le  11991  lemul1a  12000  infrelb  12132  nnadddir  12224  zextle  12593  zextlt  12594  btwnnz  12596  gtndiv  12597  uzind2  12613  fzind  12618  zsupss  12878  xrltne  13105  lemaxle  13138  qbtwnre  13142  qbtwnxr  13143  xlemul1a  13231  icogelb  13340  iccleub  13345  iccsplit  13429  uzsubsubfz  13491  elfz0fzfz0  13578  difelfznle  13587  fvffz0  13591  elfzo0le  13649  fzonmapblen  13654  fzofzim  13655  ceile  13799  modadd1  13858  muladdmodid  13863  modmul1  13877  modirr  13895  fsuppmapnn0fiub0  13946  expcl2lem  14026  expclzlem  14036  expnegz  14049  leexp2r  14127  bcval4  14260  bccmpl  14262  hashbnd  14289  hashunsnggt  14347  hashgt23el  14377  hashfundm  14395  elovmpowrd  14511  ccatval2  14531  ccatrcl1  14548  wrdl1s1  14568  ccat2s1fvw  14592  swrdsb0eq  14617  swrdccatin1  14678  pfxccatpfx2  14690  repswswrd  14737  cshwcsh2id  14781  absexpz  15258  climbdd  15625  iseraltlem2  15636  binomfallfac  15997  dvdsle  16270  divalgb  16364  ndvdssub  16369  dvdsgcd  16504  dfgcd2  16506  rplpwr  16518  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  lcmfunsn  16604  coprmdvds1  16612  qredeq  16617  2mulprm  16653  prmdvdsexpr  16678  nnnn0modprm0  16768  prm23ge5  16777  pcexp  16821  difsqpwdvds  16849  prmpwdvds  16866  ramcl  16991  cshwshashlem3  17059  cshwrepswhash1  17064  elrestr  17382  mreintcl  17548  mremre  17557  mrieqv2d  17596  initoeu2lem1  17972  funcestrcsetclem9  18105  funcsetcestrclem9  18120  prstr  18256  drsdirfi  18262  latnlej  18413  latnlej2  18416  acsdrsel  18500  acsdrscl  18503  mrelatglb  18517  mrelatlub  18519  isnmgm  18603  grpasscan1  18968  grpinvnz  18977  mulgneg2  19075  gsmsymgrfix  19394  f1omvdco2  19414  symggen  19436  odcl2  19531  odhash3  19542  lsmss1  19631  lsmss2  19633  efgred  19714  efgcpbl  19722  ablfacrp  20034  ablfac1eu  20041  ablfaclem3  20055  omndadd  20094  ogrpaddlt  20104  dvdsrmul1  20340  dvdsunit  20350  irredmul  20400  c0snmgmhm  20433  lmodlema  20855  psgnodpmr  21565  phlssphl  21634  lindsss  21799  lindfmm  21802  ply1scln0  22277  dmatelnd  22479  mdetdiaglem  22581  mdet0  22589  mdetunilem7  22601  slesolinv  22663  cramerimplem3  22668  cpmatpmat  22693  m2cpminvid2lem  22737  chfacfscmul0  22841  chfacfpmmul0  22845  riinopn  22891  clsndisj  23058  cnpf2  23233  hausnei2  23336  cmpcov  23372  cmpfii  23392  unconn  23412  t1connperf  23419  nrmr0reg  23732  fbfinnfr  23824  filuni  23868  alexsubALT  24034  tmdgsum  24078  cuspcvg  24283  mopni  24475  isngp4  24595  metdsre  24837  iimulcl  24922  phtpc01  24981  clmmulg  25086  cfilucfil4  25306  bcthlem5  25313  bcth  25314  bcth3  25316  itg1le  25698  itg2le  25724  bddmulibl  25824  bddiblnc  25827  dvnres  25916  cpnord  25920  dvnfre  25937  deg1ge  26081  dgr1term  26243  aaliou3lem2  26327  sincosq1lem  26479  cxpge0  26665  cxpmul2  26671  logrec  26745  logbgcd1irr  26776  sqfpc  27118  bcmono  27258  gausslemma2dlem1a  27346  gausslemma2dlem2  27348  gausslemma2dlem4  27350  2lgsoddprmlem3  27395  pntrmax  27545  qabvexp  27607  ostth2lem2  27615  nosepon  27647  nolesgn2o  27653  nogesgn1o  27655  nosepnelem  27661  nosepne  27662  nosepdmlem  27665  nosepdm  27666  nodenselem8  27673  noresle  27679  noetasuplem4  27718  noetainflem4  27722  cutbdaylt  27808  eqcuts3  27814  addsuniflem  28011  sltmuls1  28157  precsexlem6  28222  precsexlem7  28223  precsexlem11  28227  ltonold  28271  onnolt  28276  n0fincut  28365  oldfib  28387  expadds  28445  ax5seglem4  29019  axeuclidlem  29049  uhgredgrnv  29217  usgredg4  29304  nbuhgr2vtx1edgblem  29438  vtxduhgr0e  29565  vtxduhgr0nedg  29579  rusgrpropnb  29670  uspgr2wlkeqi  29734  redwlklem  29756  lfgrwlkprop  29772  2pthnloop  29817  spthonepeq  29838  pthdlem2lem  29853  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  crctcshwlkn0lem7  29902  crctcshwlkn0  29907  wlkiswwlks1  29953  wlkiswwlks2  29961  wlkiswwlksupgr2  29963  wwlksnext  29979  wwlksnextproplem2  29996  wspthsnonn0vne  30003  2pthon3v  30029  rusgrnumwwlk  30064  erclwwlkeqlen  30107  erclwwlksym  30109  erclwwlktr  30110  erclwwlkneqlen  30156  erclwwlknsym  30158  erclwwlkntr  30159  uhgr3cyclex  30270  upgreupthseg  30297  eupth2lem3lem4  30319  eucrctshift  30331  4cycl2vnunb  30378  nvs  30752  nvtri  30759  nmlno0  30884  nmlnoubi  30885  ubth  30962  hlipgt0  31003  ocnel  31387  elspansn2  31656  elspansn3  31661  normcan  31665  pjoml2  31700  lecm  31706  osum  31734  nmbdfnlb  32139  leopmul  32223  hstpyth  32318  cvnbtwn  32375  ssmd1  32400  ssmd2  32401  ssdmd1  32402  ssdmd2  32403  cvmd  32425  cvdmd  32426  superpos  32443  disji2f  32666  disjif  32667  disjif2  32670  preiman0  32802  padct  32810  ffs2  32819  bcm1n  32887  sgn3da  32926  s2f1  33024  archiabl  33279  slmdlema  33284  lbslsat  33800  eulerpartlemb  34552  fisshasheq  35343  cvmsdisj  35498  cvmlift2lem12  35542  satfrel  35595  satfrnmapom  35598  fmlasuc  35614  satffun  35637  satef  35644  sategoelfv  35648  lineintmo  36385  nn0prpwlem  36550  nn0prpw  36551  neibastop2lem  36588  tr0elw  36712  lindsadd  37980  areacirc  38080  incsequz  38115  mettrifi  38124  ismtybnd  38174  heiborlem1  38178  rngoisocnv  38348  risci  38354  eqvrelqsel  39067  lfl1  39562  lkrlsp2  39595  omlfh3N  39751  cvrnbtwn  39763  cvrnbtwn2  39767  cvrnbtwn4  39771  cvlexch3  39824  cvlexch4N  39825  cvlatexchb1  39826  2llnne2N  39900  atcvrj0  39920  cvrat2  39921  ps-1  39969  3atlem5  39979  islln2a  40009  lplnriaN  40042  lplnribN  40043  llncvrlpln2  40049  lplncvrlvol2  40107  psubatN  40247  pmapglb2N  40263  pmapglb2xN  40264  2llnma1b  40278  paddasslem17  40328  pmod2iN  40341  pmodl42N  40343  hlmod1i  40348  atmod1i1  40349  atmod1i2  40351  llnmod1i2  40352  pclcmpatN  40393  osumcllem8N  40455  pexmidlem3N  40464  pl42lem4N  40474  4atexlem7  40567  ltrnnid  40628  cdlemc4  40686  cdleme32a  40933  cdlemeg46gfre  41024  cdlemf2  41054  cdlemg4c  41104  trlcoat  41215  tendovalco  41257  tendoeq2  41266  cdlemk36  41405  diael  41535  diatrl  41536  dicelval1stN  41680  dicelval2nd  41681  dihlspsnat  41825  dochkr1  41970  lcfrlem9  42042  mapdh8e  42276  hdmapval0  42325  hgmapval0  42384  dvdsexpnn0  42811  incssnn0  43160  pell14qrexpcl  43312  pell14qrgap  43320  congadd  43411  acongsym  43421  acongtr  43423  dvdsacongtr  43429  jm2.19lem3  43436  jm2.19lem4  43437  jm2.26lem3  43446  onexlimgt  43688  nadd2rabex  43831  ismnushort  44745  bi13impia  44933  3impcombi  45260  ioogtlb  45940  iocgtlb  45947  iocleub  45948  icoltub  45953  iooltub  45955  limclner  46094  limsupre3lem  46175  climuzlem  46186  fsupdm  47285  finfdm  47289  elfzelfzlble  47784  subsubelfzo0  47790  m1modnep2mod  47821  m1modmmod  47827  modlt0b  47832  mod2addne  47833  iccpartigtl  47898  sqrtpwpw2p  48016  fmtnoprmfac1lem  48042  fmtno4prmfac  48050  evenltle  48208  even3prm2  48210  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem1  48296  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  uhgrimisgrgriclem  48421  isubgr3stgrlem7  48463  clnbgr3stgrgrlic  48511  gpgedg2iv  48558  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  upgrwlkupwlk  48631  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  lincscmcl  48923  lindslinindimp2lem4  48952  lincresunit2  48969  lincresunit3  48972  elfzolborelfzop1  49010  rege1logbzge0  49050  fllog2  49059  dignn0ldlem  49093  rrx2pnecoorneor  49206  rrx2plord2  49213  rrx2linest  49233  ipolub  49478  ipoglb  49481