Theorem mpanr1 701

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpanr12  703  oacl  8486  omcl  8487  oaordi  8498  oawordri  8502  oaass  8513  oarec  8514  omordi  8518  omwordri  8524  odi  8531  omass  8532  oeoelem  8550  undom  9010  fimax2g  9240  fimin2g  9442  frr1  9704  axcnre  11109  divdiv23zi  11917  recp1lt1  12062  divgt0i  12072  divge0i  12073  ltreci  12074  lereci  12075  lt2msqi  12076  le2msqi  12077  msq11i  12078  ltdiv23i  12088  ltdivp1i  12090  zmin  12878  ge0gtmnf  13101  hashprg  14305  sqrt11i  15281  sqrtmuli  15282  sqrtmsq2i  15284  sqrtlei  15285  sqrtlti  15286  cos01gt0  16084  wspthsnwspthsnon  28924  vc2OLD  29573  vc0  29579  vcm  29581  nvpi  29672  nvge0  29678  ipval3  29714  ipidsq  29715  sspmval  29738  opsqrlem1  31145  opsqrlem6  31150  hstle  31235  hstrbi  31271  atordi  31389  finorwe  35926  poimirlem6  36157  poimirlem7  36158  poimirlem16  36167  poimirlem19  36170  poimirlem20  36171