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  6391  2dom  6971  phplem4  7029  fiintim  7109  mulidnq  7592  nq0m0r  7659  nq0a0  7660  addpinq1  7667  0idsr  7970  1idsr  7971  00sr  7972  addresr  8040  mulresr  8041  pitonnlem2  8050  ax0id  8081  recexaplem2  8815  reclt1  9059  crap0  9121  nominpos  9365  expnass  10884  crim  11390  sqrt00  11572  mulcn2  11844  sin02gt0  12296  opoe  12427  oddprm  12803  pythagtriplem3  12811  pc1  12849  txswaphmeo  15016  sinq34lt0t  15526  cosordlem  15544  lgsne0  15738  lgsdinn0  15748  3dom  16465