Theorem mpanr2 700

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 525	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 592	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fvreseq1  6681  op1steq  7596  fpmg  8289  pmresg  8291  pw2f1o  8476  pm54.43  9282  dfac2b  9409  ttukeylem6  9789  gruina  10093  muleqadd  11138  divdiv1  11205  addltmul  11727  elfzp1b  12838  elfzm1b  12839  expp1z  13332  expm1  13333  oddvdsnn0  18407  efgi0  18577  efgi1  18578  fiinbas  21248  opnneissb  21410  fclscf  22321  blssec  22732  iimulcl  23228  itg2lr  24018  blocnilem  28268  lnopmul  29431  opsqrlem6  29609  gsumle  30490  gsumvsca1  30493  gsumvsca2  30494  locfinreflem  30717  fvray  33213  fvline  33216  fneref  33309  poimirlem3  34447  poimirlem16  34460  fdc  34573  linepmap  36463  rmyeq0  39056