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  8572  omcl  8573  oaordi  8583  oawordri  8587  oaass  8598  oarec  8599  omordi  8603  omwordri  8609  odi  8616  omass  8617  oeoelem  8635  undom  9098  fimax2g  9320  fimin2g  9535  frr1  9797  axcnre  11202  divdiv23zi  12018  recp1lt1  12164  divgt0i  12174  divge0i  12175  ltreci  12176  lereci  12177  lt2msqi  12178  le2msqi  12179  msq11i  12180  ltdiv23i  12190  ltdivp1i  12192  zmin  12984  ge0gtmnf  13211  hashprg  14431  sqrt11i  15420  sqrtmuli  15421  sqrtmsq2i  15423  sqrtlei  15424  sqrtlti  15425  cos01gt0  16224  wspthsnwspthsnon  29946  vc2OLD  30597  vc0  30603  vcm  30605  nvpi  30696  nvge0  30702  ipval3  30738  ipidsq  30739  sspmval  30762  opsqrlem1  32169  opsqrlem6  32174  hstle  32259  hstrbi  32295  atordi  32413  weiunlem2  36446  finorwe  37365  poimirlem6  37613  poimirlem7  37614  poimirlem16  37623  poimirlem19  37626  poimirlem20  37627