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  8535  omcl  8536  oaordi  8546  oawordri  8550  oaass  8561  oarec  8562  omordi  8566  omwordri  8572  odi  8579  omass  8580  oeoelem  8598  undom  9059  fimax2g  9289  fimin2g  9492  frr1  9754  axcnre  11159  divdiv23zi  11967  recp1lt1  12112  divgt0i  12122  divge0i  12123  ltreci  12124  lereci  12125  lt2msqi  12126  le2msqi  12127  msq11i  12128  ltdiv23i  12138  ltdivp1i  12140  zmin  12928  ge0gtmnf  13151  hashprg  14355  sqrt11i  15331  sqrtmuli  15332  sqrtmsq2i  15334  sqrtlei  15335  sqrtlti  15336  cos01gt0  16134  wspthsnwspthsnon  29170  vc2OLD  29821  vc0  29827  vcm  29829  nvpi  29920  nvge0  29926  ipval3  29962  ipidsq  29963  sspmval  29986  opsqrlem1  31393  opsqrlem6  31398  hstle  31483  hstrbi  31519  atordi  31637  finorwe  36263  poimirlem6  36494  poimirlem7  36495  poimirlem16  36504  poimirlem19  36507  poimirlem20  36508