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  2632  ceqsalt  3470  3gencl  3480  vtoclgft  3505  vtoclegft  3539  rspc6v  3593  mob2  3669  moi  3672  reupick3  4275  disjne  4400  elpr2elpr  4816  disji2  5070  disji  5071  tz7.2  5594  sofld  6129  ordintdif  6352  funopg  6510  fvun1  6908  fvopab6  6958  fveqressseq  7007  fvcofneq  7021  fprg  7083  isores3  7264  ovmpt4g  7488  ovmpos  7489  ov2gf  7490  ofrval  7617  sorpssuni  7660  sorpssint  7661  poxp  8053  poseq  8083  suppss2  8125  frrlem12  8222  smoel  8275  smoord  8280  smogt  8282  oaass  8471  oewordi  8501  oeoalem  8506  oeoelem  8508  nnawordi  8531  nnaass  8532  naddssim  8595  qsel  8715  xpdom3  8983  onsdominel  9034  mapdom3  9057  sdomdomtrfi  9105  domsdomtrfi  9106  php  9111  onomeneq  9118  fisseneq  9142  fodomfir  9207  cantnflem1  9574  ttrclss  9605  cfslbn  10153  cfsmolem  10156  cfcoflem  10158  infpssrlem4  10192  fin23lem7  10202  fin23lem25  10210  isf34lem7  10265  hsmexlem2  10313  axcc3  10324  axdc4lem  10341  tskss  10644  gruss  10682  gruurn  10684  gruiun  10685  gruel  10689  gruen  10698  grudomon  10703  grothac  10716  axpre-sup  11055  axsup  11183  addn0nid  11532  letrp1  11960  p1le  11961  lemul1a  11970  infrelb  12102  zextle  12541  zextlt  12542  btwnnz  12544  gtndiv  12545  uzind2  12561  fzind  12566  eluzsubOLD  12763  zsupss  12830  xrltne  13057  lemaxle  13089  qbtwnre  13093  qbtwnxr  13094  xlemul1a  13182  icogelb  13291  iccleub  13296  iccsplit  13380  uzsubsubfz  13441  elfz0fzfz0  13528  difelfznle  13537  fvffz0  13541  elfzo0le  13598  fzonmapblen  13603  fzofzim  13604  ceile  13748  modadd1  13807  muladdmodid  13812  modmul1  13826  modirr  13844  fsuppmapnn0fiub0  13895  expcl2lem  13975  expclzlem  13985  expnegz  13998  leexp2r  14076  bcval4  14209  bccmpl  14211  hashbnd  14238  hashunsnggt  14296  hashgt23el  14326  hashfundm  14344  elovmpowrd  14460  ccatval2  14480  ccatrcl1  14497  wrdl1s1  14517  ccat2s1fvw  14541  swrdsb0eq  14566  swrdccatin1  14627  pfxccatpfx2  14639  repswswrd  14686  cshwcsh2id  14730  absexpz  15207  climbdd  15574  iseraltlem2  15585  binomfallfac  15943  dvdsle  16216  divalgb  16310  ndvdssub  16315  dvdsgcd  16450  dfgcd2  16452  rplpwr  16464  nn0rppwr  16467  nn0expgcd  16470  lcmgcdlem  16512  lcmfunsn  16550  coprmdvds1  16558  qredeq  16563  2mulprm  16599  prmdvdsexpr  16623  nnnn0modprm0  16713  prm23ge5  16722  pcexp  16766  difsqpwdvds  16794  prmpwdvds  16811  ramcl  16936  cshwshashlem3  17004  cshwrepswhash1  17009  elrestr  17327  mreintcl  17492  mremre  17501  mrieqv2d  17540  initoeu2lem1  17916  funcestrcsetclem9  18049  funcsetcestrclem9  18064  prstr  18200  drsdirfi  18206  latnlej  18357  latnlej2  18360  acsdrsel  18444  acsdrscl  18447  mrelatglb  18461  mrelatlub  18463  isnmgm  18547  grpasscan1  18909  grpinvnz  18918  mulgneg2  19016  gsmsymgrfix  19335  f1omvdco2  19355  symggen  19377  odcl2  19472  odhash3  19483  lsmss1  19572  lsmss2  19574  efgred  19655  efgcpbl  19663  ablfacrp  19975  ablfac1eu  19982  ablfaclem3  19996  omndadd  20035  ogrpaddlt  20045  dvdsrmul1  20282  dvdsunit  20292  irredmul  20342  c0snmgmhm  20375  lmodlema  20793  psgnodpmr  21522  phlssphl  21591  lindsss  21756  lindfmm  21759  ply1scln0  22201  dmatelnd  22406  mdetdiaglem  22508  mdet0  22516  mdetunilem7  22528  slesolinv  22590  cramerimplem3  22595  cpmatpmat  22620  m2cpminvid2lem  22664  chfacfscmul0  22768  chfacfpmmul0  22772  riinopn  22818  clsndisj  22985  cnpf2  23160  hausnei2  23263  cmpcov  23299  cmpfii  23319  unconn  23339  t1connperf  23346  nrmr0reg  23659  fbfinnfr  23751  filuni  23795  alexsubALT  23961  tmdgsum  24005  cuspcvg  24210  mopni  24402  isngp4  24522  metdsre  24764  iimulcl  24855  phtpc01  24917  clmmulg  25023  cfilucfil4  25243  bcthlem5  25250  bcth  25251  bcth3  25253  itg1le  25636  itg2le  25662  bddmulibl  25762  bddiblnc  25765  dvnres  25855  cpnord  25859  dvnfre  25878  deg1ge  26025  dgr1term  26187  aaliou3lem2  26273  sincosq1lem  26428  cxpge0  26614  cxpmul2  26620  logrec  26695  logbgcd1irr  26726  sqfpc  27069  bcmono  27210  gausslemma2dlem1a  27298  gausslemma2dlem2  27300  gausslemma2dlem4  27302  2lgsoddprmlem3  27347  pntrmax  27497  qabvexp  27559  ostth2lem2  27567  nosepon  27599  nolesgn2o  27605  nogesgn1o  27607  nosepnelem  27613  nosepne  27614  nosepdmlem  27617  nosepdm  27618  nodenselem8  27625  noresle  27631  noetasuplem4  27670  noetainflem4  27674  scutbdaylt  27754  eqscut3  27760  addsuniflem  27939  ssltmul1  28081  precsexlem6  28145  precsexlem7  28146  precsexlem11  28150  sltonold  28193  onnolt  28198  n0sfincut  28277  expadds  28353  ax5seglem4  28905  axeuclidlem  28935  uhgredgrnv  29103  usgredg4  29190  nbuhgr2vtx1edgblem  29324  vtxduhgr0e  29452  vtxduhgr0nedg  29466  rusgrpropnb  29557  uspgr2wlkeqi  29621  redwlklem  29643  lfgrwlkprop  29659  2pthnloop  29704  spthonepeq  29725  pthdlem2lem  29740  crctcshwlkn0lem3  29785  crctcshwlkn0lem5  29787  crctcshwlkn0lem7  29789  crctcshwlkn0  29794  wlkiswwlks1  29840  wlkiswwlks2  29848  wlkiswwlksupgr2  29850  wwlksnext  29866  wwlksnextproplem2  29883  wspthsnonn0vne  29890  2pthon3v  29916  rusgrnumwwlk  29948  erclwwlkeqlen  29991  erclwwlksym  29993  erclwwlktr  29994  erclwwlkneqlen  30040  erclwwlknsym  30042  erclwwlkntr  30043  uhgr3cyclex  30154  upgreupthseg  30181  eupth2lem3lem4  30203  eucrctshift  30215  4cycl2vnunb  30262  nvs  30635  nvtri  30642  nmlno0  30767  nmlnoubi  30768  ubth  30845  hlipgt0  30886  ocnel  31270  elspansn2  31539  elspansn3  31544  normcan  31548  pjoml2  31583  lecm  31589  osum  31617  nmbdfnlb  32022  leopmul  32106  hstpyth  32201  cvnbtwn  32258  ssmd1  32283  ssmd2  32284  ssdmd1  32285  ssdmd2  32286  cvmd  32308  cvdmd  32309  superpos  32326  disji2f  32549  disjif  32550  disjif2  32553  preiman0  32683  padct  32693  ffs2  32702  bcm1n  32769  sgn3da  32809  s2f1  32918  archiabl  33159  slmdlema  33164  lbslsat  33621  eulerpartlemb  34373  fisshasheq  35151  cvmsdisj  35306  cvmlift2lem12  35350  satfrel  35403  satfrnmapom  35406  fmlasuc  35422  satffun  35445  satef  35452  sategoelfv  35456  lineintmo  36191  nn0prpwlem  36356  nn0prpw  36357  neibastop2lem  36394  lindsadd  37653  areacirc  37753  incsequz  37788  mettrifi  37797  ismtybnd  37847  heiborlem1  37851  rngoisocnv  38021  risci  38027  eqvrelqsel  38653  lfl1  39109  lkrlsp2  39142  omlfh3N  39298  cvrnbtwn  39310  cvrnbtwn2  39314  cvrnbtwn4  39318  cvlexch3  39371  cvlexch4N  39372  cvlatexchb1  39373  2llnne2N  39447  atcvrj0  39467  cvrat2  39468  ps-1  39516  3atlem5  39526  islln2a  39556  lplnriaN  39589  lplnribN  39590  llncvrlpln2  39596  lplncvrlvol2  39654  psubatN  39794  pmapglb2N  39810  pmapglb2xN  39811  2llnma1b  39825  paddasslem17  39875  pmod2iN  39888  pmodl42N  39890  hlmod1i  39895  atmod1i1  39896  atmod1i2  39898  llnmod1i2  39899  pclcmpatN  39940  osumcllem8N  40002  pexmidlem3N  40011  pl42lem4N  40021  4atexlem7  40114  ltrnnid  40175  cdlemc4  40233  cdleme32a  40480  cdlemeg46gfre  40571  cdlemf2  40601  cdlemg4c  40651  trlcoat  40762  tendovalco  40804  tendoeq2  40813  cdlemk36  40952  diael  41082  diatrl  41083  dicelval1stN  41227  dicelval2nd  41228  dihlspsnat  41372  dochkr1  41517  lcfrlem9  41589  mapdh8e  41823  hdmapval0  41872  hgmapval0  41931  nnadddir  42303  dvdsexpnn0  42367  incssnn0  42744  pell14qrexpcl  42900  pell14qrgap  42908  congadd  42999  acongsym  43009  acongtr  43011  dvdsacongtr  43017  jm2.19lem3  43024  jm2.19lem4  43025  jm2.26lem3  43034  onexlimgt  43276  nadd2rabex  43419  ismnushort  44334  bi13impia  44522  3impcombi  44849  ioogtlb  45535  iocgtlb  45542  iocleub  45543  icoltub  45548  iooltub  45550  limclner  45689  limsupre3lem  45770  climuzlem  45781  fsupdm  46880  finfdm  46884  elfzelfzlble  47352  subsubelfzo0  47357  m1modnep2mod  47383  m1modmmod  47389  modlt0b  47394  mod2addne  47395  iccpartigtl  47454  sqrtpwpw2p  47569  fmtnoprmfac1lem  47595  fmtno4prmfac  47603  evenltle  47748  even3prm2  47750  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  bgoldbtbndlem1  47836  bgoldbtbndlem3  47838  bgoldbtbndlem4  47839  bgoldbtbnd  47840  uhgrimisgrgriclem  47961  isubgr3stgrlem7  48003  clnbgr3stgrgrlic  48051  gpgedg2iv  48098  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem6  48155  upgrwlkupwlk  48171  funcringcsetcALTV2lem9  48329  funcringcsetclem9ALTV  48352  lincscmcl  48464  lindslinindimp2lem4  48493  lincresunit2  48510  lincresunit3  48513  elfzolborelfzop1  48551  rege1logbzge0  48591  fllog2  48600  dignn0ldlem  48634  rrx2pnecoorneor  48747  rrx2plord2  48754  rrx2linest  48774  ipolub  49019  ipoglb  49022