Theorem mp3an 914

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an.1	|- ph
mp3an.2	|- ps
mp3an.3	|- ch
mp3an.4	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an	|- th

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 |- ps
2		mp3an.3	. 2 |- ch
3		mp3an.1	. . 3 |- ph
4		mp3an.4	. . 3 |- ((ph /\ ps /\ ch) -> th)
5	3, 4	mp3an1 901	. 2 |- ((ps /\ ch) -> th)
6	1, 2, 5	mp2an 696	1 |- th

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  vtocl3 1840  ordom 3136  funopg 3539  eloprabi 4108  ondomon 4836  1lt2pi 5012  addass 5304  mulass 5305  adddi 5306  adddir 5307  add12 5320  add23 5321  addcan2 5334  addsubass 5367  addsub 5368  subcan 5393  subcan2 5394  mul23 5404  subdi 5409  subdir 5410  pnncan 5462  lttr 5567  lelttr 5568  ltletr 5569  letr 5570  ltadd2 5572  ltsubadd2 5619  lesubadd2 5620  ltaddsub 5621  divne0 5701  ltmul2 5798  lemul1 5799  lemul2 5800  ledivp1 5862  ltdivp1 5863  halfpm6th 5987  unirnioo 6343  icoshftf1oi 6350  i4 6672  abs3dif 6845  faclbnd4lem1 6893  bcpasc2 6913  bcpasc 6915  climfnrcl 7056  iserzshft 7088  climabslem 7092  serzf0 7113  fnsmntlem 7168  fnsmnt 7169  expcnvlem2 7171  geolimilem 7178  geolim1i 7181  0.999... 7189  ivthlem4 7227  ivthlem6 7229  ivthlem7 7230  ivthlem8 7231  ivthlem9 7232  isupivth 7233  dsupivthlem 7234  ivthlem4OLD 7236  ivthlem7OLD 7239  ivthlem8OLD 7240  ivth2OLD 7242  reefcl 7267  efaddlem5 7292  efaddlem6 7293  efaddlem12 7299  efaddlem20 7307  efaddlem22 7309  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  ef01tlub 7335  absef01tlub 7337  eirrlem1 7338  eirrlem2 7339  eirrlem3 7340  eirrlem4 7341  eirrlem5 7342  efsep 7345  efm1legeo 7365  efcnlem1 7367  cosadd 7402  cos2tOLD 7414  sin01bndlem1 7417  cos1bnd 7424  cos2bnd 7425  sincos1sgn 7429  sincos2sgn 7430  sin4lt0 7431  ruclem10 7470  ruclem11 7471  ruclem13 7473  xplm 7925  oprcn 7927  opr1scn 7930  bopcn 7935  issubgi 8074  ghgrpi 8089  0vfval 8177  sqcn 8283  lnocoi 8365  nmlno0lem 8398  nmblolbii 8403  blocnilem 8408  blocni 8409  cnph 8422  isph 8425  ip0i 8428  ip1ilem 8429  ip2i 8431  ipdirilem 8432  ipasslem6 8439  ipasslem9 8442  ipasslem10 8443  ipasslem11 8444  ip2dii 8448  pythi 8454  siilem1 8455  siilem2 8456  siii 8457  htthlem1 8563  htthlem6 8568  htthlem7 8569  htthlem12 8574  pilem3 8611  sinhalfpilem 8617  sincosq1lem 8639  sincosq4sgn 8643  sincos4thpi 8646  sincos6thpi 8647  cosh111lem1 8648  cosh111t 8651  efghgrpilem 8653  efifolem1 8656  efifolem3 8658  efifolem4 8659  efifolem6 8661  efif1lem5 8668  efif1lem6 8669  efif1lem7 8670  shftefif1olem 8680  resslogrn 8692  pilog 8707  hvmulass 8852  hvmulcom 8853  hvdistr1 8857  hvsubdistr1 8858  hvass 8859  hvadd23 8860  his35 8894  normlem0 8914  normlem8 8922  normlem9 8923  bcseq 8925  polid2 8963  hhph 8984  occllem1 9112  shscl 9219  h1de2 9414  pjadj 9558  pjdifnorm 9568  pjcj 9569  hoaddsubass 9686  eigre 9700  eigpos 9702  eigorth 9703  adj0 9857  lnopeq0lem1 9868  lnopunilem1 9873  lnophmlem2 9880  lnfn0 9909  nmopadjlem 9960  nmoptri 9965  nmopco 9966  nmopcoadj 9972  mdexch 10199  cayleylem3 10345

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 776

Copyright terms: Public domain