Theorem mpanr12 443

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  cnvoprab  6470  2dom  7093  phplem4  7156  fiintim  7238  mulidnq  7756  nq0m0r  7823  nq0a0  7824  addpinq1  7831  0idsr  8134  1idsr  8135  00sr  8136  addresr  8204  mulresr  8205  pitonnlem2  8214  ax0id  8245  recexaplem2  8981  reclt1  9227  crap0  9289  nominpos  9545  expnass  11084  crim  11625  sqrt00  11808  mulcn2  12080  sin02gt0  12533  opoe  12664  oddprm  13040  pythagtriplem3  13048  pc1  13086  txswaphmeo  15424  sinq34lt0t  15935  cosordlem  15953  lgsne0  16169  lgsdinn0  16179  eupth2lem3lem4fi  16726  3dom  17030