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  6386  2dom  6966  phplem4  7024  fiintim  7101  mulidnq  7584  nq0m0r  7651  nq0a0  7652  addpinq1  7659  0idsr  7962  1idsr  7963  00sr  7964  addresr  8032  mulresr  8033  pitonnlem2  8042  ax0id  8073  recexaplem2  8807  reclt1  9051  crap0  9113  nominpos  9357  expnass  10875  crim  11377  sqrt00  11559  mulcn2  11831  sin02gt0  12283  opoe  12414  oddprm  12790  pythagtriplem3  12798  pc1  12836  txswaphmeo  15003  sinq34lt0t  15513  cosordlem  15531  lgsne0  15725  lgsdinn0  15735  3dom  16381