Theorem mpanr1 703

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 701	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  705  oacl  8462  omcl  8463  oaordi  8473  oawordri  8477  oaass  8488  oarec  8489  omordi  8493  omwordri  8499  odi  8506  omass  8507  oeoelem  8526  undom  8993  fimax2g  9186  fimin2g  9402  frr1  9671  axcnre  11075  divdiv23zi  11894  recp1lt1  12040  divgt0i  12050  divge0i  12051  ltreci  12052  lereci  12053  lt2msqi  12054  le2msqi  12055  msq11i  12056  ltdiv23i  12066  ltdivp1i  12068  zmin  12857  ge0gtmnf  13087  hashprg  14318  sqrt11i  15308  sqrtmuli  15309  sqrtmsq2i  15311  sqrtlei  15312  sqrtlti  15313  cos01gt0  16116  wspthsnwspthsnon  29989  vc2OLD  30643  vc0  30649  vcm  30651  nvpi  30742  nvge0  30748  ipval3  30784  ipidsq  30785  sspmval  30808  opsqrlem1  32215  opsqrlem6  32220  hstle  32305  hstrbi  32341  atordi  32459  weiunlem  36657  finorwe  37587  poimirlem6  37827  poimirlem7  37828  poimirlem16  37837  poimirlem19  37840  poimirlem20  37841