Theorem mpanr1 719

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 681	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 717	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 197  df-an 385

This theorem is referenced by:  mpanr12  721  oacl  7660  omcl  7661  oaordi  7671  oawordri  7675  oaass  7686  oarec  7687  omordi  7691  omwordri  7697  odi  7704  omass  7705  oeoelem  7723  fimax2g  8247  fimin2g  8444  axcnre  10023  divdiv23zi  10816  recp1lt1  10959  divgt0i  10970  divge0i  10971  ltreci  10972  lereci  10973  lt2msqi  10974  le2msqi  10975  msq11i  10976  ltdiv23i  10986  ltdivp1i  10988  zmin  11822  ge0gtmnf  12041  hashprg  13220  hashprgOLD  13221  sqrt11i  14168  sqrtmuli  14169  sqrtmsq2i  14171  sqrtlei  14172  sqrtlti  14173  cos01gt0  14965  wspthsnwspthsnon  26879  vc2OLD  27551  vc0  27557  vcm  27559  nvpi  27650  nvge0  27656  ipval3  27692  ipidsq  27693  sspmval  27716  opsqrlem1  29127  opsqrlem6  29132  hstle  29217  hstrbi  29253  atordi  29371  poimirlem6  33545  poimirlem7  33546  poimirlem16  33555  poimirlem19  33558  poimirlem20  33559