Theorem mpanr12 705

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

Hypotheses

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

Assertion

Ref	Expression
mpanr12	⊢ (𝜑 → 𝜃)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 ⊢ 𝜒
2		mpanr12.1	. . 3 ⊢ 𝜓
3		mpanr12.3	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	mpanr1 703	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 691	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  wfisgOLD  6376  f1ofvswap  7325  2dom  9068  limensuci  9191  phplem4OLD  9254  fiintOLD  9364  frinsg  9788  djuen  10207  isfin1-3  10423  prlem934  11070  0idsr  11134  1idsr  11135  00sr  11136  addresr  11175  mulresr  11176  reclt1  12160  crne0  12256  nominpos  12500  fvf1tp  13825  expnass  14243  faclbnd2  14326  crim  15150  01sqrexlem1  15277  01sqrexlem7  15283  sqrt00  15298  sqreulem  15394  mulcn2  15628  ege2le3  16122  sin02gt0  16224  opoe  16396  oddprm  16843  pythagtriplem2  16850  pythagtriplem3  16851  pythagtriplem16  16863  pythagtrip  16867  pc1  16888  prmlem0  17139  acsfn0  17704  mgpress  20166  mgpressOLD  20167  abvneg  20843  pmatcollpw3  22805  leordtval2  23235  txswaphmeo  23828  iccntr  24856  dvlipcn  26047  sinq34lt0t  26565  cosordlem  26586  efif1olem3  26600  lgamgulmlem2  27087  basellem3  27140  ppiub  27262  bposlem9  27350  lgsne0  27393  lgsdinn0  27403  chebbnd1  27530  eupth2lem3lem4  30259  mayete3i  31756  lnop0  31994  nmcexi  32054  nmoptrii  32122  nmopcoadji  32129  hstle1  32254  hst0  32261  strlem5  32283  jplem1  32296  cnvoprabOLD  32737  subfacp1lem5  35168  limsucncmpi  36427  matunitlindflem1  37602  poimirlem15  37621  dvasin  37690  fdc  37731  eldioph3b  42752  oaabsb  43283  tfsconcatfv2  43329  or2expropbi  46983  ich2exprop  47395  sprsymrelfolem2  47417  clnbgrisubgrgrim  47837  sinhpcosh  48970