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  8536  omcl  8537  oaordi  8547  oawordri  8551  oaass  8562  oarec  8563  omordi  8567  omwordri  8573  odi  8580  omass  8581  oeoelem  8600  undom  9077  fimax2g  9270  fimin2g  9484  frr1  9756  axcnre  11242  divdiv23zi  12063  recp1lt1  12208  divgt0i  12218  divge0i  12219  ltreci  12220  lereci  12221  lt2msqi  12222  le2msqi  12223  msq11i  12224  ltdiv23i  12234  ltdivp1i  12236  zmin  13064  ge0gtmnf  13295  hashprg  14532  sqrt11i  15545  sqrtmuli  15546  sqrtmsq2i  15548  sqrtlei  15549  sqrtlti  15550  cos01gt0  16352  wspthsnwspthsnon  30498  vc2OLD  31163  vc0  31169  vcm  31171  nvpi  31262  nvge0  31268  ipval3  31304  ipidsq  31305  sspmval  31328  opsqrlem1  32735  opsqrlem6  32740  hstle  32825  hstrbi  32861  atordi  32979  weiunlem  37231  finorwe  38285  poimirlem6  38524  poimirlem7  38525  poimirlem16  38534  poimirlem19  38537  poimirlem20  38538