Theorem mpanr12 703

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 701	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 689	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  wfisgOLD  6357  f1ofvswap  7309  2dom  9056  limensuci  9181  phplem4OLD  9245  unfiOLD  9338  fiintOLD  9360  frinsg  9785  djuen  10203  isfin1-3  10418  prlem934  11065  0idsr  11129  1idsr  11130  00sr  11131  addresr  11170  mulresr  11171  reclt1  12153  crne0  12249  nominpos  12493  expnass  14218  faclbnd2  14301  crim  15113  01sqrexlem1  15240  01sqrexlem7  15246  sqrt00  15261  sqreulem  15357  mulcn2  15591  ege2le3  16085  sin02gt0  16187  opoe  16358  oddprm  16805  pythagtriplem2  16812  pythagtriplem3  16813  pythagtriplem16  16825  pythagtrip  16829  pc1  16850  prmlem0  17101  acsfn0  17666  mgpress  20126  mgpressOLD  20127  abvneg  20799  pmatcollpw3  22772  leordtval2  23202  txswaphmeo  23795  iccntr  24823  dvlipcn  26013  sinq34lt0t  26532  cosordlem  26552  efif1olem3  26566  lgamgulmlem2  27053  basellem3  27106  ppiub  27228  bposlem9  27316  lgsne0  27359  lgsdinn0  27369  chebbnd1  27496  eupth2lem3lem4  30159  mayete3i  31656  lnop0  31894  nmcexi  31954  nmoptrii  32022  nmopcoadji  32029  hstle1  32154  hst0  32161  strlem5  32183  jplem1  32196  cnvoprabOLD  32632  subfacp1lem5  35023  limsucncmpi  36168  matunitlindflem1  37328  poimirlem15  37347  dvasin  37416  fdc  37457  eldioph3b  42457  oaabsb  42995  tfsconcatfv2  43041  or2expropbi  46683  ich2exprop  47077  sprsymrelfolem2  47099  clnbgrisubgrgrim  47513  sinhpcosh  48520