Theorem mpanr1 702

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpanr12  704  oacl  8530  omcl  8531  oaordi  8542  oawordri  8546  oaass  8557  oarec  8558  omordi  8562  omwordri  8568  odi  8575  omass  8576  oeoelem  8594  undom  9055  fimax2g  9285  fimin2g  9488  frr1  9750  axcnre  11155  divdiv23zi  11963  recp1lt1  12108  divgt0i  12118  divge0i  12119  ltreci  12120  lereci  12121  lt2msqi  12122  le2msqi  12123  msq11i  12124  ltdiv23i  12134  ltdivp1i  12136  zmin  12924  ge0gtmnf  13147  hashprg  14351  sqrt11i  15327  sqrtmuli  15328  sqrtmsq2i  15330  sqrtlei  15331  sqrtlti  15332  cos01gt0  16130  wspthsnwspthsnon  29150  vc2OLD  29799  vc0  29805  vcm  29807  nvpi  29898  nvge0  29904  ipval3  29940  ipidsq  29941  sspmval  29964  opsqrlem1  31371  opsqrlem6  31376  hstle  31461  hstrbi  31497  atordi  31615  finorwe  36201  poimirlem6  36432  poimirlem7  36433  poimirlem16  36442  poimirlem19  36445  poimirlem20  36446