Theorem mpanr1 704

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 702	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  706  oacl  8472  omcl  8473  oaordi  8483  oawordri  8487  oaass  8498  oarec  8499  omordi  8503  omwordri  8509  odi  8516  omass  8517  oeoelem  8536  undom  9005  fimax2g  9198  fimin2g  9414  frr1  9683  axcnre  11087  divdiv23zi  11906  recp1lt1  12052  divgt0i  12062  divge0i  12063  ltreci  12064  lereci  12065  lt2msqi  12066  le2msqi  12067  msq11i  12068  ltdiv23i  12078  ltdivp1i  12080  zmin  12869  ge0gtmnf  13099  hashprg  14330  sqrt11i  15320  sqrtmuli  15321  sqrtmsq2i  15323  sqrtlei  15324  sqrtlti  15325  cos01gt0  16128  wspthsnwspthsnon  30001  vc2OLD  30655  vc0  30661  vcm  30663  nvpi  30754  nvge0  30760  ipval3  30796  ipidsq  30797  sspmval  30820  opsqrlem1  32227  opsqrlem6  32232  hstle  32317  hstrbi  32353  atordi  32471  weiunlem  36676  finorwe  37634  poimirlem6  37874  poimirlem7  37875  poimirlem16  37884  poimirlem19  37887  poimirlem20  37888