Theorem mpanr1 716

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanr12  718  oacl  8522  omcl  8523  oaordi  8533  oawordri  8537  oaass  8548  oarec  8549  omordi  8553  omwordri  8559  odi  8566  omass  8567  oeoelem  8586  undom  9056  fimax2g  9249  fimin2g  9462  frr1  9734  axcnre  11160  divdiv23zi  11979  recp1lt1  12124  divgt0i  12134  divge0i  12135  ltreci  12136  lereci  12137  lt2msqi  12138  le2msqi  12139  msq11i  12140  ltdiv23i  12150  ltdivp1i  12152  zmin  12980  ge0gtmnf  13210  hashprg  14445  sqrt11i  15456  sqrtmuli  15457  sqrtmsq2i  15459  sqrtlei  15460  sqrtlti  15461  cos01gt0  16265  wspthsnwspthsnon  30308  vc2OLD  30967  vc0  30973  vcm  30975  nvpi  31066  nvge0  31072  ipval3  31108  ipidsq  31109  sspmval  31132  opsqrlem1  32539  opsqrlem6  32544  hstle  32629  hstrbi  32665  atordi  32783  weiunlem  37007  finorwe  38061  poimirlem6  38310  poimirlem7  38311  poimirlem16  38320  poimirlem19  38323  poimirlem20  38324