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  8450  omcl  8451  oaordi  8461  oawordri  8465  oaass  8476  oarec  8477  omordi  8481  omwordri  8487  odi  8494  omass  8495  oeoelem  8513  undom  8978  fimax2g  9170  fimin2g  9383  frr1  9652  axcnre  11055  divdiv23zi  11874  recp1lt1  12020  divgt0i  12030  divge0i  12031  ltreci  12032  lereci  12033  lt2msqi  12034  le2msqi  12035  msq11i  12036  ltdiv23i  12046  ltdivp1i  12048  zmin  12842  ge0gtmnf  13071  hashprg  14302  sqrt11i  15292  sqrtmuli  15293  sqrtmsq2i  15295  sqrtlei  15296  sqrtlti  15297  cos01gt0  16100  wspthsnwspthsnon  29895  vc2OLD  30546  vc0  30552  vcm  30554  nvpi  30645  nvge0  30651  ipval3  30687  ipidsq  30688  sspmval  30711  opsqrlem1  32118  opsqrlem6  32123  hstle  32208  hstrbi  32244  atordi  32362  weiunlem2  36503  finorwe  37422  poimirlem6  37672  poimirlem7  37673  poimirlem16  37682  poimirlem19  37685  poimirlem20  37686