Theorem mpanr1 703

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanr12  705  oacl  8459  omcl  8460  oaordi  8470  oawordri  8474  oaass  8485  oarec  8486  omordi  8490  omwordri  8496  odi  8503  omass  8504  oeoelem  8522  undom  8989  fimax2g  9181  fimin2g  9394  frr1  9663  axcnre  11066  divdiv23zi  11885  recp1lt1  12031  divgt0i  12041  divge0i  12042  ltreci  12043  lereci  12044  lt2msqi  12045  le2msqi  12046  msq11i  12047  ltdiv23i  12057  ltdivp1i  12059  zmin  12848  ge0gtmnf  13078  hashprg  14309  sqrt11i  15299  sqrtmuli  15300  sqrtmsq2i  15302  sqrtlei  15303  sqrtlti  15304  cos01gt0  16107  wspthsnwspthsnon  29915  vc2OLD  30569  vc0  30575  vcm  30577  nvpi  30668  nvge0  30674  ipval3  30710  ipidsq  30711  sspmval  30734  opsqrlem1  32141  opsqrlem6  32146  hstle  32231  hstrbi  32267  atordi  32385  weiunlem2  36579  finorwe  37499  poimirlem6  37739  poimirlem7  37740  poimirlem16  37749  poimirlem19  37752  poimirlem20  37753