Theorem mpanr1 695

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  mpanr12  697  oacl  7856  omcl  7857  oaordi  7867  oawordri  7871  oaass  7882  oarec  7883  omordi  7887  omwordri  7893  odi  7900  omass  7901  oeoelem  7919  fimax2g  8449  fimin2g  8646  axcnre  10274  divdiv23zi  11071  recp1lt1  11214  divgt0i  11225  divge0i  11226  ltreci  11227  lereci  11228  lt2msqi  11229  le2msqi  11230  msq11i  11231  ltdiv23i  11241  ltdivp1i  11243  zmin  12028  ge0gtmnf  12251  hashprg  13431  sqrt11i  14464  sqrtmuli  14465  sqrtmsq2i  14467  sqrtlei  14468  sqrtlti  14469  cos01gt0  15256  wspthsnwspthsnon  27202  vc2OLD  27947  vc0  27953  vcm  27955  nvpi  28046  nvge0  28052  ipval3  28088  ipidsq  28089  sspmval  28112  opsqrlem1  29523  opsqrlem6  29528  hstle  29613  hstrbi  29649  atordi  29767  poimirlem6  33903  poimirlem7  33904  poimirlem16  33913  poimirlem19  33916  poimirlem20  33917