Theorem mpanr1 702

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

Hypotheses

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

Assertion

Ref	Expression
mpanr1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2 ⊢ 𝜓
2		mpanr1.2	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	anassrs 467	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 700	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanr12  704  oacl  8591  omcl  8592  oaordi  8602  oawordri  8606  oaass  8617  oarec  8618  omordi  8622  omwordri  8628  odi  8635  omass  8636  oeoelem  8654  undom  9125  fimax2g  9350  fimin2g  9566  frr1  9828  axcnre  11233  divdiv23zi  12047  recp1lt1  12193  divgt0i  12203  divge0i  12204  ltreci  12205  lereci  12206  lt2msqi  12207  le2msqi  12208  msq11i  12209  ltdiv23i  12219  ltdivp1i  12221  zmin  13009  ge0gtmnf  13234  hashprg  14444  sqrt11i  15433  sqrtmuli  15434  sqrtmsq2i  15436  sqrtlei  15437  sqrtlti  15438  cos01gt0  16239  wspthsnwspthsnon  29949  vc2OLD  30600  vc0  30606  vcm  30608  nvpi  30699  nvge0  30705  ipval3  30741  ipidsq  30742  sspmval  30765  opsqrlem1  32172  opsqrlem6  32177  hstle  32262  hstrbi  32298  atordi  32416  weiunlem2  36429  finorwe  37348  poimirlem6  37586  poimirlem7  37587  poimirlem16  37596  poimirlem19  37599  poimirlem20  37600