Theorem mpanr1 716

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanr12  718  oacl  8547  omcl  8548  oaordi  8558  oawordri  8562  oaass  8573  oarec  8574  omordi  8578  omwordri  8584  odi  8591  omass  8592  oeoelem  8611  undom  9088  fimax2g  9281  fimin2g  9495  frr1  9767  axcnre  11253  divdiv23zi  12074  recp1lt1  12219  divgt0i  12229  divge0i  12230  ltreci  12231  lereci  12232  lt2msqi  12233  le2msqi  12234  msq11i  12235  ltdiv23i  12245  ltdivp1i  12247  zmin  13075  ge0gtmnf  13306  hashprg  14543  sqrt11i  15558  sqrtmuli  15559  sqrtmsq2i  15561  sqrtlei  15562  sqrtlti  15563  cos01gt0  16365  wspthsnwspthsnon  30511  vc2OLD  31176  vc0  31182  vcm  31184  nvpi  31275  nvge0  31281  ipval3  31317  ipidsq  31318  sspmval  31341  opsqrlem1  32748  opsqrlem6  32753  hstle  32838  hstrbi  32874  atordi  32992  weiunlem  37344  finorwe  38399  poimirlem6  38638  poimirlem7  38639  poimirlem16  38648  poimirlem19  38651  poimirlem20  38652