Theorem mpdan 703

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpdan.1	|- (ph -> ps)
mpdan.2	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mpdan	|- (ph -> ch)

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		mpdan.1	. 2 |- (ph -> ps)
2		mpdan.2	. . 3 |- ((ph /\ ps) -> ch)
3	2	ex 373	. 2 |- (ph -> (ps -> ch))
4	1, 3	mpd 26	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpancom 704  mpd3an3 915  eueq2 1914  eueq3 1915  csbiegf 2027  csbnestglem 2031  csbidmg 2035  reuunisn 2890  onsucuni 3080  elrnopabg 3791  fnressn 3828  elrnoprabg 4114  oaordi 4170  oaabs 4242  dom2d 4391  canth2g 4471  php4 4502  onfin 4505  pwfilem 4550  pwfi 4551  supsnALT 4572  infeq5 4601  trcl 4625  oncardval 4799  cardonle 4802  canth3 4830  cardaleph 4865  cfval 4886  reclem3pr 5138  reclem4pr 5139  0idsr 5186  lecase 5603  lep1t 5776  ledivp1t 5861  xrsupss 6033  xrinfmss 6034  zbtwnre 6177  flhalft 6197  ceiget 6199  ceim1lt 6200  qbtwnre 6224  ser1add2 6283  ser1add 6284  ioossre 6336  uz11t 6372  fzneuzt 6458  expubndt 6547  reim0t 6719  absnegt 6775  abscjt 6777  sqabsaddt 6791  sqabssubt 6792  leabst 6807  cvg3 6868  faclbnd4lem3 6895  faclbnd4lem4 6896  bcn0t 6909  bcnnt 6910  fsum1ps 6964  fsumsplit 6966  binomlem5 7016  climconst2 7040  climrecl 7055  climge0 7057  isumcmpi 7158  efaddlem6 7293  efcant 7318  reeff1o 7376  resin4pt 7386  recos4pt 7387  sincossqt 7411  tgvalt 7566  cctop 7602  cldval 7616  ntrfval 7617  clsfval 7618  cldcls 7632  cmclsopn 7643  neifval 7664  lpfval 7692  cncnplem4 7727  blfval 7787  ssblex 7808  opnfval 7809  tgioolem 7866  lmfval 7877  caufval 7878  lmuni 7902  opr1cn 7928  opr2cn 7929  bopcnlem2 7932  bcthlem16 7964  isgrpi 7992  grpidval 8008  grpinvfval 8016  grpinvid 8024  grpdivfval 8031  issubg 8068  cnaddabl 8078  vcz 8141  vcoprne 8150  nvz0 8248  sspz 8341  lno0 8364  0lno 8395  ipasslem2 8435  sincolem 8603  shftefif1olem 8680  ococint 9235  spanvalt 9237  shunss 9275  pjocin 9583  nmcopexlem6 9894  lncnopbd 9904  nmcfnexlem6 9923  riesz3 9933  cnlnadjlem7 9944  hmopidmpj 10018  pjclem4 10065  pj3s 10073  hstoct 10087  hstnmoct 10088  hstoht 10097  hst0t 10098  mdsl2 10186  irredlem3 10256  irredlem4 10257  dmdbr5at 10284  ghomgrpilem2 10320  ghomid 10328  homeofval 10439  idhme 10445  hmphre 10453  mslb1 10509  cnvtr 10518  imonclem 10619

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

Copyright terms: Public domain