Theorem mpanr1 715

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanr12  717  oacl  8516  omcl  8517  oaordi  8527  oawordri  8531  oaass  8542  oarec  8543  omordi  8547  omwordri  8553  odi  8560  omass  8561  oeoelem  8580  undom  9049  fimax2g  9242  fimin2g  9455  frr1  9727  axcnre  11145  divdiv23zi  11964  recp1lt1  12109  divgt0i  12119  divge0i  12120  ltreci  12121  lereci  12122  lt2msqi  12123  le2msqi  12124  msq11i  12125  ltdiv23i  12135  ltdivp1i  12137  zmin  12964  ge0gtmnf  13194  hashprg  14427  sqrt11i  15432  sqrtmuli  15433  sqrtmsq2i  15435  sqrtlei  15436  sqrtlti  15437  cos01gt0  16243  wspthsnwspthsnon  30202  vc2OLD  30857  vc0  30863  vcm  30865  nvpi  30956  nvge0  30962  ipval3  30998  ipidsq  30999  sspmval  31022  opsqrlem1  32429  opsqrlem6  32434  hstle  32519  hstrbi  32555  atordi  32673  weiunlem  36859  finorwe  37911  poimirlem6  38160  poimirlem7  38161  poimirlem16  38170  poimirlem19  38173  poimirlem20  38174