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  8499  omcl  8500  oaordi  8510  oawordri  8514  oaass  8525  oarec  8526  omordi  8530  omwordri  8536  odi  8543  omass  8544  oeoelem  8562  undom  9029  fimax2g  9233  fimin2g  9450  frr1  9712  axcnre  11117  divdiv23zi  11935  recp1lt1  12081  divgt0i  12091  divge0i  12092  ltreci  12093  lereci  12094  lt2msqi  12095  le2msqi  12096  msq11i  12097  ltdiv23i  12107  ltdivp1i  12109  zmin  12903  ge0gtmnf  13132  hashprg  14360  sqrt11i  15351  sqrtmuli  15352  sqrtmsq2i  15354  sqrtlei  15355  sqrtlti  15356  cos01gt0  16159  wspthsnwspthsnon  29846  vc2OLD  30497  vc0  30503  vcm  30505  nvpi  30596  nvge0  30602  ipval3  30638  ipidsq  30639  sspmval  30662  opsqrlem1  32069  opsqrlem6  32074  hstle  32159  hstrbi  32195  atordi  32313  weiunlem2  36451  finorwe  37370  poimirlem6  37620  poimirlem7  37621  poimirlem16  37630  poimirlem19  37633  poimirlem20  37634