Theorem mpanr2 716

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
mpanr2	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpanr2

Step	Hyp	Ref	Expression
1		mpanr2.1	. . 3 ⊢ 𝜒
2	1	jctr 563	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 490	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  fvreseq1  6211  op1steq  7079  fpmg  7747  pmresg  7749  pw2f1o  7928  pm54.43  8687  dfac2  8814  ttukeylem6  9197  gruina  9497  muleqadd  10523  divdiv1  10588  addltmul  11118  elfzp1b  12244  elfzm1b  12245  expp1z  12729  expm1  12730  oddvdsnn0  17735  efgi0  17905  efgi1  17906  fiinbas  20515  opnneissb  20676  fclscf  21587  blssec  21998  iimulcl  22492  itg2lr  23248  blocnilem  26837  lnopmul  28004  opsqrlem6  28182  gsumle  28904  gsumvsca1  28907  gsumvsca2  28908  locfinreflem  29029  fvray  31212  fvline  31215  fneref  31309  poimirlem3  32376  poimirlem16  32389  fdc  32505  linepmap  33873  rmyeq0  36332