Theorem mpanr1 703

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 471	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 701	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mpanr12  705  oacl  8184  omcl  8185  oaordi  8196  oawordri  8200  oaass  8211  oarec  8212  omordi  8216  omwordri  8222  odi  8229  omass  8230  oeoelem  8248  fimax2g  8831  fimin2g  9027  axcnre  10657  divdiv23zi  11464  recp1lt1  11609  divgt0i  11619  divge0i  11620  ltreci  11621  lereci  11622  lt2msqi  11623  le2msqi  11624  msq11i  11625  ltdiv23i  11635  ltdivp1i  11637  zmin  12419  ge0gtmnf  12641  hashprg  13841  sqrt11i  14827  sqrtmuli  14828  sqrtmsq2i  14830  sqrtlei  14831  sqrtlti  14832  cos01gt0  15629  wspthsnwspthsnon  27846  vc2OLD  28495  vc0  28501  vcm  28503  nvpi  28594  nvge0  28600  ipval3  28636  ipidsq  28637  sspmval  28660  opsqrlem1  30067  opsqrlem6  30072  hstle  30157  hstrbi  30193  atordi  30311  frr1  33454  finorwe  35165  poimirlem6  35395  poimirlem7  35396  poimirlem16  35405  poimirlem19  35408  poimirlem20  35409