Theorem mpanr12 721

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses

Ref	Expression
mpanr12.1	⊢ 𝜓
mpanr12.2	⊢ 𝜒
mpanr12.3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr12	⊢ (𝜑 → 𝜃)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 ⊢ 𝜒
2		mpanr12.1	. . 3 ⊢ 𝜓
3		mpanr12.3	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	mpanr1 719	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 707	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  wfisg  5753  2dom  8070  limensuci  8177  phplem4  8183  unfi  8268  fiint  8278  cdaen  9033  isfin1-3  9246  prlem934  9893  0idsr  9956  1idsr  9957  00sr  9958  addresr  9997  mulresr  9998  reclt1  10956  crne0  11051  nominpos  11307  expnass  13010  faclbnd2  13118  crim  13899  sqrlem1  14027  sqrlem7  14033  sqrt00  14048  sqreulem  14143  mulcn2  14370  ege2le3  14864  sin02gt0  14966  opoe  15134  oddprm  15562  pythagtriplem2  15569  pythagtriplem3  15570  pythagtriplem16  15582  pythagtrip  15586  pc1  15607  prmlem0  15859  acsfn0  16368  mgpress  18546  abvneg  18882  pmatcollpw3  20637  leordtval2  21064  txswaphmeo  21656  iccntr  22671  dvlipcn  23802  sinq34lt0t  24306  cosordlem  24322  efif1olem3  24335  lgamgulmlem2  24801  basellem3  24854  ppiub  24974  bposlem9  25062  lgsne0  25105  lgsdinn0  25115  chebbnd1  25206  eupth2lem3lem4  27209  mayete3i  28715  lnop0  28953  nmcexi  29013  nmoptrii  29081  nmopcoadji  29088  hstle1  29213  hst0  29220  strlem5  29242  jplem1  29255  cnvoprabOLD  29626  subfacp1lem5  31292  frinsg  31870  limsucncmpi  32569  matunitlindflem1  33535  poimirlem15  33554  dvasin  33626  fdc  33671  eldioph3b  37645  sprsymrelfolem2  42068  sinhpcosh  42809