Theorem 3impia 1118

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  mopick2  2638  ceqsalt  3476  3gencl  3486  vtoclgft  3511  vtoclegft  3545  rspc6v  3599  mob2  3675  moi  3678  reupick3  4284  disjne  4409  elpr2elpr  4827  disji2  5084  disji  5085  tz7.2  5615  sofld  6153  ordintdif  6376  funopg  6534  fvun1  6933  fvopab6  6984  fveqressseq  7033  fvcofneq  7047  fprg  7110  isores3  7291  ovmpt4g  7515  ovmpos  7516  ov2gf  7517  ofrval  7644  sorpssuni  7687  sorpssint  7688  poxp  8080  poseq  8110  suppss2  8152  frrlem12  8249  smoel  8302  smoord  8307  smogt  8309  oaass  8498  oewordi  8529  oeoalem  8534  oeoelem  8536  nnawordi  8559  nnaass  8560  naddssim  8623  qsel  8745  xpdom3  9015  onsdominel  9066  mapdom3  9089  sdomdomtrfi  9137  domsdomtrfi  9138  php  9143  onomeneq  9150  fisseneq  9175  fodomfir  9240  cantnflem1  9610  ttrclss  9641  cfslbn  10189  cfsmolem  10192  cfcoflem  10194  infpssrlem4  10228  fin23lem7  10238  fin23lem25  10246  isf34lem7  10301  hsmexlem2  10349  axcc3  10360  axdc4lem  10377  tskss  10681  gruss  10719  gruurn  10721  gruiun  10722  gruel  10726  gruen  10735  grudomon  10740  grothac  10753  axpre-sup  11092  axsup  11220  addn0nid  11569  letrp1  11997  p1le  11998  lemul1a  12007  infrelb  12139  zextle  12577  zextlt  12578  btwnnz  12580  gtndiv  12581  uzind2  12597  fzind  12602  zsupss  12862  xrltne  13089  lemaxle  13122  qbtwnre  13126  qbtwnxr  13127  xlemul1a  13215  icogelb  13324  iccleub  13329  iccsplit  13413  uzsubsubfz  13474  elfz0fzfz0  13561  difelfznle  13570  fvffz0  13574  elfzo0le  13631  fzonmapblen  13636  fzofzim  13637  ceile  13781  modadd1  13840  muladdmodid  13845  modmul1  13859  modirr  13877  fsuppmapnn0fiub0  13928  expcl2lem  14008  expclzlem  14018  expnegz  14031  leexp2r  14109  bcval4  14242  bccmpl  14244  hashbnd  14271  hashunsnggt  14329  hashgt23el  14359  hashfundm  14377  elovmpowrd  14493  ccatval2  14513  ccatrcl1  14530  wrdl1s1  14550  ccat2s1fvw  14574  swrdsb0eq  14599  swrdccatin1  14660  pfxccatpfx2  14672  repswswrd  14719  cshwcsh2id  14763  absexpz  15240  climbdd  15607  iseraltlem2  15618  binomfallfac  15976  dvdsle  16249  divalgb  16343  ndvdssub  16348  dvdsgcd  16483  dfgcd2  16485  rplpwr  16497  nn0rppwr  16500  nn0expgcd  16503  lcmgcdlem  16545  lcmfunsn  16583  coprmdvds1  16591  qredeq  16596  2mulprm  16632  prmdvdsexpr  16656  nnnn0modprm0  16746  prm23ge5  16755  pcexp  16799  difsqpwdvds  16827  prmpwdvds  16844  ramcl  16969  cshwshashlem3  17037  cshwrepswhash1  17042  elrestr  17360  mreintcl  17526  mremre  17535  mrieqv2d  17574  initoeu2lem1  17950  funcestrcsetclem9  18083  funcsetcestrclem9  18098  prstr  18234  drsdirfi  18240  latnlej  18391  latnlej2  18394  acsdrsel  18478  acsdrscl  18481  mrelatglb  18495  mrelatlub  18497  isnmgm  18581  grpasscan1  18943  grpinvnz  18952  mulgneg2  19050  gsmsymgrfix  19369  f1omvdco2  19389  symggen  19411  odcl2  19506  odhash3  19517  lsmss1  19606  lsmss2  19608  efgred  19689  efgcpbl  19697  ablfacrp  20009  ablfac1eu  20016  ablfaclem3  20030  omndadd  20069  ogrpaddlt  20079  dvdsrmul1  20317  dvdsunit  20327  irredmul  20377  c0snmgmhm  20410  lmodlema  20828  psgnodpmr  21557  phlssphl  21626  lindsss  21791  lindfmm  21794  ply1scln0  22246  dmatelnd  22452  mdetdiaglem  22554  mdet0  22562  mdetunilem7  22574  slesolinv  22636  cramerimplem3  22641  cpmatpmat  22666  m2cpminvid2lem  22710  chfacfscmul0  22814  chfacfpmmul0  22818  riinopn  22864  clsndisj  23031  cnpf2  23206  hausnei2  23309  cmpcov  23345  cmpfii  23365  unconn  23385  t1connperf  23392  nrmr0reg  23705  fbfinnfr  23797  filuni  23841  alexsubALT  24007  tmdgsum  24051  cuspcvg  24256  mopni  24448  isngp4  24568  metdsre  24810  iimulcl  24901  phtpc01  24963  clmmulg  25069  cfilucfil4  25289  bcthlem5  25296  bcth  25297  bcth3  25299  itg1le  25682  itg2le  25708  bddmulibl  25808  bddiblnc  25811  dvnres  25901  cpnord  25905  dvnfre  25924  deg1ge  26071  dgr1term  26233  aaliou3lem2  26319  sincosq1lem  26474  cxpge0  26660  cxpmul2  26666  logrec  26741  logbgcd1irr  26772  sqfpc  27115  bcmono  27256  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem4  27348  2lgsoddprmlem3  27393  pntrmax  27543  qabvexp  27605  ostth2lem2  27613  nosepon  27645  nolesgn2o  27651  nogesgn1o  27653  nosepnelem  27659  nosepne  27660  nosepdmlem  27663  nosepdm  27664  nodenselem8  27671  noresle  27677  noetasuplem4  27716  noetainflem4  27720  cutbdaylt  27806  eqcuts3  27812  addsuniflem  28009  sltmuls1  28155  precsexlem6  28220  precsexlem7  28221  precsexlem11  28225  ltonold  28269  onnolt  28274  n0fincut  28363  oldfib  28385  expadds  28443  ax5seglem4  29017  axeuclidlem  29047  uhgredgrnv  29215  usgredg4  29302  nbuhgr2vtx1edgblem  29436  vtxduhgr0e  29564  vtxduhgr0nedg  29578  rusgrpropnb  29669  uspgr2wlkeqi  29733  redwlklem  29755  lfgrwlkprop  29771  2pthnloop  29816  spthonepeq  29837  pthdlem2lem  29852  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  crctcshwlkn0lem7  29901  crctcshwlkn0  29906  wlkiswwlks1  29952  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wwlksnext  29978  wwlksnextproplem2  29995  wspthsnonn0vne  30002  2pthon3v  30028  rusgrnumwwlk  30063  erclwwlkeqlen  30106  erclwwlksym  30108  erclwwlktr  30109  erclwwlkneqlen  30155  erclwwlknsym  30157  erclwwlkntr  30158  uhgr3cyclex  30269  upgreupthseg  30296  eupth2lem3lem4  30318  eucrctshift  30330  4cycl2vnunb  30377  nvs  30751  nvtri  30758  nmlno0  30883  nmlnoubi  30884  ubth  30961  hlipgt0  31002  ocnel  31386  elspansn2  31655  elspansn3  31660  normcan  31664  pjoml2  31699  lecm  31705  osum  31733  nmbdfnlb  32138  leopmul  32222  hstpyth  32317  cvnbtwn  32374  ssmd1  32399  ssmd2  32400  ssdmd1  32401  ssdmd2  32402  cvmd  32424  cvdmd  32425  superpos  32442  disji2f  32664  disjif  32665  disjif2  32668  preiman0  32800  padct  32808  ffs2  32817  bcm1n  32886  sgn3da  32926  s2f1  33038  archiabl  33292  slmdlema  33297  lbslsat  33794  eulerpartlemb  34546  fisshasheq  35331  cvmsdisj  35486  cvmlift2lem12  35530  satfrel  35583  satfrnmapom  35586  fmlasuc  35602  satffun  35625  satef  35632  sategoelfv  35636  lineintmo  36373  nn0prpwlem  36538  nn0prpw  36539  neibastop2lem  36576  lindsadd  37864  areacirc  37964  incsequz  37999  mettrifi  38008  ismtybnd  38058  heiborlem1  38062  rngoisocnv  38232  risci  38238  eqvrelqsel  38951  lfl1  39446  lkrlsp2  39479  omlfh3N  39635  cvrnbtwn  39647  cvrnbtwn2  39651  cvrnbtwn4  39655  cvlexch3  39708  cvlexch4N  39709  cvlatexchb1  39710  2llnne2N  39784  atcvrj0  39804  cvrat2  39805  ps-1  39853  3atlem5  39863  islln2a  39893  lplnriaN  39926  lplnribN  39927  llncvrlpln2  39933  lplncvrlvol2  39991  psubatN  40131  pmapglb2N  40147  pmapglb2xN  40148  2llnma1b  40162  paddasslem17  40212  pmod2iN  40225  pmodl42N  40227  hlmod1i  40232  atmod1i1  40233  atmod1i2  40235  llnmod1i2  40236  pclcmpatN  40277  osumcllem8N  40339  pexmidlem3N  40348  pl42lem4N  40358  4atexlem7  40451  ltrnnid  40512  cdlemc4  40570  cdleme32a  40817  cdlemeg46gfre  40908  cdlemf2  40938  cdlemg4c  40988  trlcoat  41099  tendovalco  41141  tendoeq2  41150  cdlemk36  41289  diael  41419  diatrl  41420  dicelval1stN  41564  dicelval2nd  41565  dihlspsnat  41709  dochkr1  41854  lcfrlem9  41926  mapdh8e  42160  hdmapval0  42209  hgmapval0  42268  nnadddir  42640  dvdsexpnn0  42704  incssnn0  43068  pell14qrexpcl  43224  pell14qrgap  43232  congadd  43323  acongsym  43333  acongtr  43335  dvdsacongtr  43341  jm2.19lem3  43348  jm2.19lem4  43349  jm2.26lem3  43358  onexlimgt  43600  nadd2rabex  43743  ismnushort  44657  bi13impia  44845  3impcombi  45172  ioogtlb  45855  iocgtlb  45862  iocleub  45863  icoltub  45868  iooltub  45870  limclner  46009  limsupre3lem  46090  climuzlem  46101  fsupdm  47200  finfdm  47204  elfzelfzlble  47681  subsubelfzo0  47686  m1modnep2mod  47712  m1modmmod  47718  modlt0b  47723  mod2addne  47724  iccpartigtl  47783  sqrtpwpw2p  47898  fmtnoprmfac1lem  47924  fmtno4prmfac  47932  evenltle  48077  even3prm2  48079  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem1  48165  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  uhgrimisgrgriclem  48290  isubgr3stgrlem7  48332  clnbgr3stgrgrlic  48380  gpgedg2iv  48427  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  upgrwlkupwlk  48500  funcringcsetcALTV2lem9  48658  funcringcsetclem9ALTV  48681  lincscmcl  48792  lindslinindimp2lem4  48821  lincresunit2  48838  lincresunit3  48841  elfzolborelfzop1  48879  rege1logbzge0  48919  fllog2  48928  dignn0ldlem  48962  rrx2pnecoorneor  49075  rrx2plord2  49082  rrx2linest  49102  ipolub  49347  ipoglb  49350