Theorem mpanr1 701

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 468	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 699	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 206  df-an 397

This theorem is referenced by:  mpanr12  703  oacl  8537  omcl  8538  oaordi  8548  oawordri  8552  oaass  8563  oarec  8564  omordi  8568  omwordri  8574  odi  8581  omass  8582  oeoelem  8600  undom  9061  fimax2g  9291  fimin2g  9494  frr1  9756  axcnre  11161  divdiv23zi  11971  recp1lt1  12116  divgt0i  12126  divge0i  12127  ltreci  12128  lereci  12129  lt2msqi  12130  le2msqi  12131  msq11i  12132  ltdiv23i  12142  ltdivp1i  12144  zmin  12932  ge0gtmnf  13155  hashprg  14359  sqrt11i  15335  sqrtmuli  15336  sqrtmsq2i  15338  sqrtlei  15339  sqrtlti  15340  cos01gt0  16138  wspthsnwspthsnon  29425  vc2OLD  30076  vc0  30082  vcm  30084  nvpi  30175  nvge0  30181  ipval3  30217  ipidsq  30218  sspmval  30241  opsqrlem1  31648  opsqrlem6  31653  hstle  31738  hstrbi  31774  atordi  31892  finorwe  36566  poimirlem6  36797  poimirlem7  36798  poimirlem16  36807  poimirlem19  36810  poimirlem20  36811