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  9063  fimax2g  9256  fimin2g  9469  frr1  9741  axcnre  11173  divdiv23zi  11992  recp1lt1  12137  divgt0i  12147  divge0i  12148  ltreci  12149  lereci  12150  lt2msqi  12151  le2msqi  12152  msq11i  12153  ltdiv23i  12163  ltdivp1i  12165  zmin  12993  ge0gtmnf  13224  hashprg  14459  sqrt11i  15472  sqrtmuli  15473  sqrtmsq2i  15475  sqrtlei  15476  sqrtlti  15477  cos01gt0  16279  wspthsnwspthsnon  30384  vc2OLD  31049  vc0  31055  vcm  31057  nvpi  31148  nvge0  31154  ipval3  31190  ipidsq  31191  sspmval  31214  opsqrlem1  32621  opsqrlem6  32626  hstle  32711  hstrbi  32747  atordi  32865  weiunlem  37082  finorwe  38136  poimirlem6  38375  poimirlem7  38376  poimirlem16  38385  poimirlem19  38388  poimirlem20  38389