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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanr12  703  oacl  8160  omcl  8161  oaordi  8172  oawordri  8176  oaass  8187  oarec  8188  omordi  8192  omwordri  8198  odi  8205  omass  8206  oeoelem  8224  fimax2g  8764  fimin2g  8961  axcnre  10586  divdiv23zi  11393  recp1lt1  11538  divgt0i  11548  divge0i  11549  ltreci  11550  lereci  11551  lt2msqi  11552  le2msqi  11553  msq11i  11554  ltdiv23i  11564  ltdivp1i  11566  zmin  12345  ge0gtmnf  12566  hashprg  13757  sqrt11i  14744  sqrtmuli  14745  sqrtmsq2i  14747  sqrtlei  14748  sqrtlti  14749  cos01gt0  15544  wspthsnwspthsnon  27695  vc2OLD  28345  vc0  28351  vcm  28353  nvpi  28444  nvge0  28450  ipval3  28486  ipidsq  28487  sspmval  28510  opsqrlem1  29917  opsqrlem6  29922  hstle  30007  hstrbi  30043  atordi  30161  frr1  33144  finorwe  34666  poimirlem6  34913  poimirlem7  34914  poimirlem16  34923  poimirlem19  34926  poimirlem20  34927