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  8463  omcl  8464  oaordi  8474  oawordri  8478  oaass  8489  oarec  8490  omordi  8494  omwordri  8500  odi  8507  omass  8508  oeoelem  8527  undom  8996  fimax2g  9189  fimin2g  9405  frr1  9674  axcnre  11078  divdiv23zi  11899  recp1lt1  12045  divgt0i  12055  divge0i  12056  ltreci  12057  lereci  12058  lt2msqi  12059  le2msqi  12060  msq11i  12061  ltdiv23i  12071  ltdivp1i  12073  zmin  12885  ge0gtmnf  13115  hashprg  14348  sqrt11i  15338  sqrtmuli  15339  sqrtmsq2i  15341  sqrtlei  15342  sqrtlti  15343  cos01gt0  16149  wspthsnwspthsnon  29999  vc2OLD  30654  vc0  30660  vcm  30662  nvpi  30753  nvge0  30759  ipval3  30795  ipidsq  30796  sspmval  30819  opsqrlem1  32226  opsqrlem6  32231  hstle  32316  hstrbi  32352  atordi  32470  weiunlem  36661  finorwe  37712  poimirlem6  37961  poimirlem7  37962  poimirlem16  37971  poimirlem19  37974  poimirlem20  37975