Theorem mpanr1 709

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 468	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 707	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpanr12  711  oacl  8460  omcl  8461  oaordi  8471  oawordri  8475  oaass  8486  oarec  8487  omordi  8491  omwordri  8497  odi  8504  omass  8505  oeoelem  8524  undom  8993  fimax2g  9186  fimin2g  9402  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  30002  vc2OLD  30657  vc0  30663  vcm  30665  nvpi  30756  nvge0  30762  ipval3  30798  ipidsq  30799  sspmval  30822  opsqrlem1  32229  opsqrlem6  32234  hstle  32319  hstrbi  32355  atordi  32473  weiunlem  36691  finorwe  37744  poimirlem6  37993  poimirlem7  37994  poimirlem16  38003  poimirlem19  38006  poimirlem20  38007