Theorem mpanr1 703

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanr12  705  oacl  8552  omcl  8553  oaordi  8563  oawordri  8567  oaass  8578  oarec  8579  omordi  8583  omwordri  8589  odi  8596  omass  8597  oeoelem  8615  undom  9078  fimax2g  9299  fimin2g  9516  frr1  9778  axcnre  11183  divdiv23zi  11999  recp1lt1  12145  divgt0i  12155  divge0i  12156  ltreci  12157  lereci  12158  lt2msqi  12159  le2msqi  12160  msq11i  12161  ltdiv23i  12171  ltdivp1i  12173  zmin  12965  ge0gtmnf  13193  hashprg  14418  sqrt11i  15408  sqrtmuli  15409  sqrtmsq2i  15411  sqrtlei  15412  sqrtlti  15413  cos01gt0  16214  wspthsnwspthsnon  29903  vc2OLD  30554  vc0  30560  vcm  30562  nvpi  30653  nvge0  30659  ipval3  30695  ipidsq  30696  sspmval  30719  opsqrlem1  32126  opsqrlem6  32131  hstle  32216  hstrbi  32252  atordi  32370  weiunlem2  36486  finorwe  37405  poimirlem6  37655  poimirlem7  37656  poimirlem16  37665  poimirlem19  37668  poimirlem20  37669