Theorem mp3an3 1452

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

This theorem is referenced by:  mp3an13  1454  mp3an23  1455  mp3anl3  1459  el3v3  3459  opelxp  5677  ov  7536  ovmpoa  7547  ovmpo  7552  frecseq123  8264  oaword1  8519  oneo  8548  oeoalem  8563  oeoelem  8565  nnaword1  8596  nnneo  8622  erov  8790  enrefg  8958  f1imaen  8991  mapxpen  9113  0sdom1dom  9192  acnlem  10008  djucomen  10138  nnadju  10158  infmap  10536  canthnumlem  10608  tskin  10719  tsksn  10720  tsk0  10723  gruxp  10767  gruina  10778  genpprecl  10961  addsrpr  11035  mulsrpr  11036  supsrlem  11071  mulrid  11179  00id  11356  mul02lem1  11357  ltneg  11685  leneg  11688  suble0  11699  div1  11879  nnaddcl  12216  nnmulcl  12217  nnge1  12221  nnsub  12237  2halves  12407  halfaddsub  12422  addltmul  12425  fcdmnn0fsuppg  12509  zleltp1  12591  nnaddm1cl  12598  zextlt  12615  eluzp1p1  12828  uzaddcl  12870  znq  12918  xrre  13136  xrre2  13137  fzshftral  13583  fraclt1  13771  expadd  14076  expmul  14079  sqmul  14091  expubnd  14150  bernneq  14201  faclbnd2  14263  faclbnd6  14271  hashgadd  14349  hashun2  14355  hashunsnggt  14366  hashssdif  14384  hashfun  14409  ccatlcan  14690  ccatrcan  14691  pfx2  14920  shftval3  15049  01sqrexlem1  15215  caubnd2  15331  bpoly2  16030  bpoly3  16031  fsumcube  16033  efexp  16076  efival  16127  cos01gt0  16166  odd2np1  16318  halfleoddlt  16339  omoe  16341  opeo  16342  divalglem5  16374  sqgcd  16539  nn0seqcvgd  16547  prmdvdssq  16695  phiprmpw  16753  eulerthlem2  16759  odzcllem  16770  pythagtriplem15  16807  pythagtriplem17  16809  pcelnn  16848  4sqlem3  16928  fullfunc  17877  fthfunc  17878  prfcl  18171  curf1cl  18196  curfcl  18200  hofcl  18227  odinv  19498  lsmelvalix  19578  dprdval  19942  lsp0  20922  lss0v  20930  zndvds0  21467  frlmlbs  21713  lindfres  21739  lmisfree  21758  coe1scl  22180  ntrin  22955  lpsscls  23035  restperf  23078  txuni2  23459  txopn  23496  elqtop2  23595  xkocnv  23708  ptcmp  23952  xblpnfps  24290  xblpnf  24291  bl2in  24295  unirnblps  24314  unirnbl  24315  blpnfctr  24331  dscopn  24468  bcthlem4  25234  minveclem2  25333  minveclem4  25339  icombl  25472  i1fadd  25603  i1fmul  25604  dvn1  25835  dvexp3  25889  plyconst  26118  plyid  26121  sincosq1eq  26428  sinord  26450  cxpp1  26596  cxpsqrtlem  26618  cxpsqrt  26619  angneg  26720  dcubic  26763  issqf  27053  ppiub  27122  bposlem1  27202  bposlem2  27203  bposlem9  27210  nosupno  27622  nosupfv  27625  noinfno  27637  noinffv  27640  scutval  27719  scutun12  27729  cuteq0  27751  cuteq1  27753  cofcut1  27835  cofcutr  27839  addscut2  27893  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  negscut2  27953  mulsproplem12  28037  mulscut2  28043  divs1  28114  precsexlem10  28125  precsexlem11  28126  bdayon  28180  n0s0suc  28241  nnzsubs  28280  zmulscld  28292  axlowdimlem6  28881  axlowdimlem14  28889  axcontlem2  28899  pthdlem2  29705  0ewlk  30050  ipasslem1  30767  ipasslem2  30768  ipasslem11  30776  minvecolem2  30811  minvecolem3  30812  minvecolem4  30816  shsva  31256  h1datomi  31517  lnfnmuli  31980  leopsq  32065  nmopleid  32075  opsqrlem6  32081  pjnmopi  32084  hstle  32166  csmdsymi  32270  atcvatlem  32321  dpfrac1  32819  cshf1o  32891  cycpmconjslem2  33119  rspidlid  33353  elsx  34191  dya2iocnrect  34279  cvmliftphtlem  35311  satfv1  35357  satffunlem1lem2  35397  satffunlem1  35401  wlimeq12  35814  fvray  36136  fvline  36139  tailfb  36372  uncov  37602  tan2h  37613  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem32  37653  mblfinlem4  37661  mbfresfi  37667  mbfposadd  37668  itg2addnc  37675  ftc1anclem5  37698  ftc1anclem8  37701  dvasin  37705  heiborlem7  37818  igenidl  38064  atlatmstc  39319  dihglblem2N  41295  eldioph4b  42806  diophren  42808  rmxp1  42928  rmyp1  42929  rmxm1  42930  rmym1  42931  dfgric2  47919  gpgov  48037  dig0  48599  i0oii  48912  iinfconstbas  49059  onetansqsecsq  49754  cotsqcscsq  49755