Theorem mp3an13 1481

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

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

Assertion

Ref	Expression
mp3an13	⊢ (𝜓 → 𝜃)

Proof of Theorem mp3an13

Step	Hyp	Ref	Expression
1		mp3an13.1	. 2 ⊢ 𝜑
2		mp3an13.2	. . 3 ⊢ 𝜒
3		mp3an13.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1479	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 703	1 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  predeq2  6297  wrecseq2  8313  oeoalem  8584  mulrid  11263  addltmul  12537  fz01en  13640  fznatpl1  13666  expubnd  14275  bernneq  14326  bernneq2  14327  faclbnd4lem1  14390  hashfun  14535  bpoly2  16176  bpoly3  16177  fsumcube  16179  efi4p  16258  efival  16273  cos2tsin  16300  cos01bnd  16307  cos01gt0  16312  dvds0  16394  odd2np1  16464  opoe  16486  divalglem0  16516  gcdid  16650  pythagtriplem4  16944  ressid  17369  fvpr0o  17678  fvpr1o  17679  zringcyg  21722  lecldbas  23484  blssioo  25061  tgioo  25062  rerest  25070  xrrest  25074  zdis  25083  reconnlem2  25094  metdscn2  25124  negcncf  25190  iihalf2  25201  cncmet  25590  rrxmvallem  25672  rrxmval  25673  ovolunlem1a  25764  ismbf3d  25922  c1lip2  26265  pilem2  26728  pilem3  26729  sinperlem  26758  sincosq1sgn  26776  sincosq2sgn  26777  sinq12gt0  26785  cosq14gt0  26788  cosq14ge0  26789  coseq1  26802  sinord  26811  zetacvg  27291  1sgmprm  27475  ppiub  27480  chtublem  27487  chtub  27488  bcp1ctr  27555  bpos1lem  27558  bposlem2  27561  bposlem3  27562  bposlem4  27563  bposlem5  27564  bposlem6  27565  bposlem7  27566  bposlem9  27568  nnsge1  28648  pw2gt0divsd  28750  pw2ge0divsd  28751  pw2ltdivmulsd  28755  pw2ltmuldivs2d  28756  pw2ltdivmuls2d  28762  pw2cut  28765  bdayfinbndlem1  28772  axlowdim  29458  ipidsq  31231  ipasslem1  31352  ipasslem2  31353  ipasslem4  31355  ipasslem5  31356  ipasslem8  31358  ipasslem9  31359  ipasslem11  31361  pjoc1i  31952  h1de2bi  32075  h1de2ctlem  32076  spanunsni  32100  opsqrlem1  32661  opsqrlem6  32666  chrelati  32885  chrelat2i  32886  cvexchlem  32889  pnfinf  33663  1fldgenq  33803  rrhre  34572  erdszelem5  35875  wsuceq2  36494  taupilem1  38156  finxpreclem2  38227  sin2h  38447  cos2h  38448  tan2h  38449  poimirlem27  38479  poimirlem30  38482  broucube  38486  mblfinlem1  38489  heiborlem6  38664  lcmineqlem19  43011  onexomgt  44180  omabs2  44271  icccncfext  46813  dirkertrigeq  47027  pgnbgreunbgrlem4  49133  zlmodzxzel  49383  dignn0flhalflem1  49643  2arymaptfo  49682  fv1prop  49727  fv2prop  49728  line2x  49782  onetansqsecsq  50770  cotsqcscsq  50771