Theorem mp3an 1191

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 1178	. 2 |- ((ps /\ ch) -> th)
6	1, 2, 5	mp2an 761	1 |- th

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  vtocl3 2342  vtocl3OLD 2343  ordom 3960  ordomOLD 3961  funopg 4454  eloprabi 5060  fparlem3 5083  fparlem4 5084  hartog 5693  ondomon 6008  1lt2pi 6184  addassi 6477  mulassi 6478  adddii 6479  adddiri 6480  add12i 6494  add23i 6495  addcan2i 6509  addsubassi 6546  addsubi 6547  subcani 6573  subcan2i 6574  mul12i 6585  mul23i 6587  subdii 6592  subdiri 6593  pnncani 6649  lttri 6760  lelttri 6761  ltletri 6762  letri 6763  ltadd2i 6765  ltsubadd2i 6821  lesubadd2i 6822  ltaddsubi 6823  divne0i 6913  ltmul2iOLD 7016  lemul1i 7017  lemul2i 7018  ledivp1i 7089  halfpm6th 7218  unirnioo 7571  icoshftf1oii 7578  expnass 7886  i4 7984  abs3difi 8152  faclbnd4lem1 8200  bcpasc2i 8219  bcpasci 8221  climfnrcli 8371  iserzshfti 8404  climabslem 8408  serzf0i 8429  arisumilem 8486  arisumi 8487  expcnvlem2 8489  geolimilem 8497  geolim1i 8500  0.999... 8508  ivthlem4 8546  ivthlem6 8548  ivthlem7 8549  ivthlem8 8550  ivthlem9 8551  isupivthi 8552  dsupivthlem 8553  reefcli 8579  efaddlem5 8604  efaddlem6 8605  efaddlem12 8611  efaddlem20 8619  efaddlem22 8621  ef1tllem 8643  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  ef01tlubi 8648  absef01tlubi 8650  eirrlem1 8651  eirrlem2 8652  eirrlem3 8653  eirrlem4 8654  eirrlem5 8655  efsepi 8661  efm1legeoi 8682  efcnlem1 8684  cosaddi 8717  cos2OLD 8730  sin01bndlem1 8733  cos1bnd 8740  cos2bnd 8741  sincos1sgn 8745  sincos2sgn 8746  sin4lt0 8747  ruclem10 8788  ruclem11 8789  ruclem13 8791  xplm 9253  oprcn 9255  opr1scn 9258  bopcn 9263  issubgi 9431  ghgrpi 9445  0vfval 9557  vacnlem6 9672  sqcn 9674  lnocoi 9757  nmlno0lem 9793  nmblolbii 9799  blocnilem 9804  blocni 9805  cnph 9819  isph 9822  ip0i 9825  ip1ilem 9826  ip2i 9828  ipdirilem 9829  ipasslem6 9836  ipasslem9 9839  ipasslem10 9840  ipasslem11 9841  ip2dii 9845  pythi 9851  siilem1 9852  siilem2 9853  siii 9854  htthlem1 9967  htthlem6 9972  htthlem7 9973  htthlem12 9978  pilem3 10022  sinhalfpilem 10028  sincosq1lem 10052  sincosq4sgn 10056  sincos4thpi 10060  sincos6thpi 10061  cosh111lem1 10068  cosh111 10071  efghgrpilem 10073  efifolem1 10076  efifolem3 10078  efifolem4 10079  efifolem6 10081  efif1lem5 10088  efif1lem6 10089  efif1lem7 10090  shftefif1olem 10095  resslogrn 10107  pilog 10122  zrdivrng 10418  hvmulassi 10545  hvmulcomi 10546  hvdistr1i 10550  hvsubdistr1i 10551  hvassi 10552  hvadd23i 10553  his35i 10588  normlem0 10608  normlem8 10616  normlem9 10617  bcseqi 10619  polid2i 10657  hhph 10678  occllem1 10806  shscli 10914  h1de2i 11109  pjadjii 11253  pjdifnormii 11263  pjcji 11264  hoaddsubassi 11383  eigrei 11397  eigposi 11399  eigorthi 11400  adj0 11556  lnopeq0lem1 11567  lnopunilem1 11572  lnophmlem2 11579  lnfn0i 11608  nmopadjlem 11659  nmoptrii 11664  nmopcoi 11665  nmopcoadji 11671  mdexchi 11907  bnj897 12817  bnj920 12827  cayleylem3 13643  dvdslelem 13692  divalglem2 13698  divalglem7 13702  gcdaddmlem 13734  2prm 13779  3prm 13780  brtxp 14067  prj1 14395  vecval3b 14795  eqindhome 14895  cntrsetlem 14999  issubcat 15193  hartogOLD 15384  fsumltisumii 15822  fsumleisumii 15825  trirni 15833  icoopnst 15876  iocopnst 15877  oprpiece1res1 15880  oprpiece1res2 15881  cncfco 15887  piececn 15894  cncfres 15895  cnresoprab 15915  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  txmet 15925  bfplem4 16001  bfplem7 16004  bfp 16009  phtpyid 16049  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpyco 16056  reparphtlem2 16064  reparpht 16065  pcoval1 16074  pcoval2 16075  pcocn 16076  pcohtpylem1 16080  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1gp 16095  stb2val1 16735  stb2val2 16736  stb3val1 16739  stb3val2 16740  stb3val3 16741  stb3xpl 16743

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 164  df-an 242  df-3an 860

Copyright terms: Public domain