Theorem mpanr12 439

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 437	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 425	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  cnvoprab  6370  2dom  6948  phplem4  7004  fiintim  7081  mulidnq  7564  nq0m0r  7631  nq0a0  7632  addpinq1  7639  0idsr  7942  1idsr  7943  00sr  7944  addresr  8012  mulresr  8013  pitonnlem2  8022  ax0id  8053  recexaplem2  8787  reclt1  9031  crap0  9093  nominpos  9337  expnass  10854  crim  11355  sqrt00  11537  mulcn2  11809  sin02gt0  12261  opoe  12392  oddprm  12768  pythagtriplem3  12776  pc1  12814  txswaphmeo  14980  sinq34lt0t  15490  cosordlem  15508  lgsne0  15702  lgsdinn0  15712