Theorem mpanr1 704

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 702	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  706  oacl  8470  omcl  8471  oaordi  8481  oawordri  8485  oaass  8496  oarec  8497  omordi  8501  omwordri  8507  odi  8514  omass  8515  oeoelem  8534  undom  9003  fimax2g  9196  fimin2g  9412  frr1  9683  axcnre  11087  divdiv23zi  11908  recp1lt1  12054  divgt0i  12064  divge0i  12065  ltreci  12066  lereci  12067  lt2msqi  12068  le2msqi  12069  msq11i  12070  ltdiv23i  12080  ltdivp1i  12082  zmin  12894  ge0gtmnf  13124  hashprg  14357  sqrt11i  15347  sqrtmuli  15348  sqrtmsq2i  15350  sqrtlei  15351  sqrtlti  15352  cos01gt0  16158  wspthsnwspthsnon  29984  vc2OLD  30639  vc0  30645  vcm  30647  nvpi  30738  nvge0  30744  ipval3  30780  ipidsq  30781  sspmval  30804  opsqrlem1  32211  opsqrlem6  32216  hstle  32301  hstrbi  32337  atordi  32455  weiunlem  36645  finorwe  37698  poimirlem6  37947  poimirlem7  37948  poimirlem16  37957  poimirlem19  37960  poimirlem20  37961