Theorem mpanr12 705

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 703	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 691	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:  wfisgOLD  6375  f1ofvswap  7326  2dom  9070  limensuci  9193  phplem4OLD  9257  fiintOLD  9367  frinsg  9791  djuen  10210  isfin1-3  10426  prlem934  11073  0idsr  11137  1idsr  11138  00sr  11139  addresr  11178  mulresr  11179  reclt1  12163  crne0  12259  nominpos  12503  fvf1tp  13829  expnass  14247  faclbnd2  14330  crim  15154  01sqrexlem1  15281  01sqrexlem7  15287  sqrt00  15302  sqreulem  15398  mulcn2  15632  ege2le3  16126  sin02gt0  16228  opoe  16400  oddprm  16848  pythagtriplem2  16855  pythagtriplem3  16856  pythagtriplem16  16868  pythagtrip  16872  pc1  16893  prmlem0  17143  acsfn0  17703  mgpress  20147  abvneg  20827  pmatcollpw3  22790  leordtval2  23220  txswaphmeo  23813  iccntr  24843  dvlipcn  26033  sinq34lt0t  26551  cosordlem  26572  efif1olem3  26586  lgamgulmlem2  27073  basellem3  27126  ppiub  27248  bposlem9  27336  lgsne0  27379  lgsdinn0  27389  chebbnd1  27516  eupth2lem3lem4  30250  mayete3i  31747  lnop0  31985  nmcexi  32045  nmoptrii  32113  nmopcoadji  32120  hstle1  32245  hst0  32252  strlem5  32274  jplem1  32287  subfacp1lem5  35189  limsucncmpi  36446  matunitlindflem1  37623  poimirlem15  37642  dvasin  37711  fdc  37752  eldioph3b  42776  oaabsb  43307  tfsconcatfv2  43353  omssaxinf2  45005  or2expropbi  47046  ich2exprop  47458  sprsymrelfolem2  47480  clnbgrisubgrgrim  47900  sinhpcosh  49259