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  8521  omcl  8522  oaordi  8532  oawordri  8536  oaass  8547  oarec  8548  omordi  8552  omwordri  8558  odi  8565  omass  8566  oeoelem  8585  undom  9054  fimax2g  9247  fimin2g  9460  frr1  9732  axcnre  11150  divdiv23zi  11969  recp1lt1  12114  divgt0i  12124  divge0i  12125  ltreci  12126  lereci  12127  lt2msqi  12128  le2msqi  12129  msq11i  12130  ltdiv23i  12140  ltdivp1i  12142  zmin  12969  ge0gtmnf  13199  hashprg  14433  sqrt11i  15438  sqrtmuli  15439  sqrtmsq2i  15441  sqrtlei  15442  sqrtlti  15443  cos01gt0  16248  wspthsnwspthsnon  30246  vc2OLD  30901  vc0  30907  vcm  30909  nvpi  31000  nvge0  31006  ipval3  31042  ipidsq  31043  sspmval  31066  opsqrlem1  32473  opsqrlem6  32478  hstle  32563  hstrbi  32599  atordi  32717  weiunlem  36955  finorwe  38009  poimirlem6  38258  poimirlem7  38259  poimirlem16  38268  poimirlem19  38271  poimirlem20  38272