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  8581  omcl  8582  oaordi  8592  oawordri  8596  oaass  8607  oarec  8608  omordi  8612  omwordri  8618  odi  8625  omass  8626  oeoelem  8645  undom  9122  fimax2g  9315  fimin2g  9528  frr1  9800  axcnre  11288  divdiv23zi  12110  recp1lt1  12255  divgt0i  12265  divge0i  12266  ltreci  12267  lereci  12268  lt2msqi  12269  le2msqi  12270  msq11i  12271  ltdiv23i  12281  ltdivp1i  12283  zmin  13111  ge0gtmnf  13342  hashprg  14580  sqrt11i  15596  sqrtmuli  15597  sqrtmsq2i  15599  sqrtlei  15600  sqrtlti  15601  cos01gt0  16403  wspthsnwspthsnon  30562  vc2OLD  31227  vc0  31233  vcm  31235  nvpi  31326  nvge0  31332  ipval3  31368  ipidsq  31369  sspmval  31392  opsqrlem1  32799  opsqrlem6  32804  hstle  32889  hstrbi  32925  atordi  33043  jltalephlem  36066  weiunlem  37466  finorwe  38573  poimirlem6  38812  poimirlem7  38813  poimirlem16  38822  poimirlem19  38825  poimirlem20  38826  grpcanonhfstruct  46299