Theorem mpanr1 699

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 697	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 206  df-an 396

This theorem is referenced by:  mpanr12  701  oacl  8327  omcl  8328  oaordi  8339  oawordri  8343  oaass  8354  oarec  8355  omordi  8359  omwordri  8365  odi  8372  omass  8373  oeoelem  8391  fimax2g  8990  fimin2g  9186  frr1  9448  axcnre  10851  divdiv23zi  11658  recp1lt1  11803  divgt0i  11813  divge0i  11814  ltreci  11815  lereci  11816  lt2msqi  11817  le2msqi  11818  msq11i  11819  ltdiv23i  11829  ltdivp1i  11831  zmin  12613  ge0gtmnf  12835  hashprg  14038  sqrt11i  15024  sqrtmuli  15025  sqrtmsq2i  15027  sqrtlei  15028  sqrtlti  15029  cos01gt0  15828  wspthsnwspthsnon  28182  vc2OLD  28831  vc0  28837  vcm  28839  nvpi  28930  nvge0  28936  ipval3  28972  ipidsq  28973  sspmval  28996  opsqrlem1  30403  opsqrlem6  30408  hstle  30493  hstrbi  30529  atordi  30647  finorwe  35480  poimirlem6  35710  poimirlem7  35711  poimirlem16  35720  poimirlem19  35723  poimirlem20  35724