Theorem mp3an3 1449

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1120	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an13  1451  mp3an23  1452  mp3anl3  1456  opelxp  5712  ov  7555  ovmpoa  7566  ovmpo  7571  frecseq123  8273  oaword1  8558  oneo  8587  oeoalem  8602  oeoelem  8604  nnaword1  8635  nnneo  8660  erov  8814  enrefg  8986  f1imaen  9018  mapxpen  9149  0sdom1dom  9244  acnlem  10049  djucomen  10178  nnadju  10198  infmap  10577  canthnumlem  10649  tskin  10760  tsksn  10761  tsk0  10764  gruxp  10808  gruina  10819  genpprecl  11002  addsrpr  11076  mulsrpr  11077  supsrlem  11112  mulrid  11219  00id  11396  mul02lem1  11397  ltneg  11721  leneg  11724  suble0  11735  div1  11910  nnaddcl  12242  nnmulcl  12243  nnge1  12247  nnsub  12263  2halves  12447  halfaddsub  12452  addltmul  12455  fcdmnn0fsuppg  12538  zleltp1  12620  nnaddm1cl  12626  zextlt  12643  eluzp1p1  12857  uzaddcl  12895  znq  12943  xrre  13155  xrre2  13156  fzshftral  13596  fraclt1  13774  expadd  14077  expmul  14080  sqmul  14091  expubnd  14149  bernneq  14199  faclbnd2  14258  faclbnd6  14266  hashgadd  14344  hashun2  14350  hashunsnggt  14361  hashssdif  14379  hashfun  14404  ccatlcan  14675  ccatrcan  14676  pfx2  14905  shftval3  15030  01sqrexlem1  15196  caubnd2  15311  bpoly2  16008  bpoly3  16009  fsumcube  16011  efexp  16051  efival  16102  cos01gt0  16141  odd2np1  16291  halfleoddlt  16312  omoe  16314  opeo  16315  divalglem5  16347  sqgcd  16509  nn0seqcvgd  16514  prmdvdssq  16662  phiprmpw  16716  eulerthlem2  16722  odzcllem  16732  pythagtriplem15  16769  pythagtriplem17  16771  pcelnn  16810  4sqlem3  16890  fullfunc  17866  fthfunc  17867  prfcl  18165  curf1cl  18191  curfcl  18195  hofcl  18222  odinv  19477  lsmelvalix  19557  dprdval  19921  lsp0  20852  lss0v  20860  zndvds0  21416  frlmlbs  21662  lindfres  21688  lmisfree  21707  coe1scl  22129  ntrin  22885  lpsscls  22965  restperf  23008  txuni2  23389  txopn  23426  elqtop2  23525  xkocnv  23638  ptcmp  23882  xblpnfps  24221  xblpnf  24222  bl2in  24226  unirnblps  24245  unirnbl  24246  blpnfctr  24262  dscopn  24402  bcthlem4  25175  minveclem2  25274  minveclem4  25280  icombl  25413  i1fadd  25544  i1fmul  25545  dvn1  25776  dvexp3  25830  plyconst  26058  plyid  26061  sincosq1eq  26362  sinord  26383  cxpp1  26528  cxpsqrtlem  26550  cxpsqrt  26551  angneg  26649  dcubic  26692  issqf  26981  ppiub  27050  bposlem1  27130  bposlem2  27131  bposlem9  27138  nosupno  27549  nosupfv  27552  noinfno  27564  noinffv  27567  scutval  27646  scutun12  27656  cuteq0  27678  cuteq1  27679  cofcut1  27753  cofcutr  27757  addscut2  27809  sleadd1  27819  addsuniflem  27831  addsasslem1  27833  addsasslem2  27834  negscut2  27865  mulsproplem12  27940  mulscut2  27946  divs1  28016  precsexlem10  28027  precsexlem11  28028  axlowdimlem6  28638  axlowdimlem14  28646  axcontlem2  28656  pthdlem2  29458  0ewlk  29800  ipasslem1  30517  ipasslem2  30518  ipasslem11  30526  minvecolem2  30561  minvecolem3  30562  minvecolem4  30566  shsva  31006  h1datomi  31267  lnfnmuli  31730  leopsq  31815  nmopleid  31825  opsqrlem6  31831  pjnmopi  31834  hstle  31916  csmdsymi  32020  atcvatlem  32071  dpfrac1  32491  cshf1o  32559  cycpmconjslem2  32750  rspidlid  32927  elsx  33656  dya2iocnrect  33744  cvmliftphtlem  34772  satfv1  34818  satffunlem1lem2  34858  satffunlem1  34862  wlimeq12  35261  fvray  35583  fvline  35586  tailfb  35726  uncov  36933  tan2h  36944  matunitlindflem1  36948  matunitlindflem2  36949  poimirlem32  36984  mblfinlem4  36992  mbfresfi  36998  mbfposadd  36999  itg2addnc  37006  ftc1anclem5  37029  ftc1anclem8  37032  dvasin  37036  heiborlem7  37149  igenidl  37395  el3v3  37553  atlatmstc  38653  dihglblem2N  40629  2xp3dxp2ge1d  41489  factwoffsmonot  41490  eldioph4b  42012  diophren  42014  rmxp1  42134  rmyp1  42135  rmxm1  42136  rmym1  42137  dig0  47454  i0oii  47714  onetansqsecsq  47968  cotsqcscsq  47969