Theorem mpdan 706

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 707  mpd3an3 919  eueq2 1921  eueq3 1922  csbiegf 2034  csbnestglem 2038  csbidmg 2042  reuunisn 2901  onsucuni 3091  elrnopabg 3806  fnressn 3843  elrnoprabg 4130  oaordi 4186  oaabs 4258  dom2d 4410  canth2g 4491  php4 4523  pwfilem 4577  pwfilemOLD 4578  pwfi 4579  pwfiOLD 4580  supsnALT 4601  infeq5 4630  trcl 4655  oncardval 4829  cardonle 4832  canth3 4861  cardaleph 4896  cfval 4918  reclem3pr 5170  reclem4pr 5171  0idsr 5218  lecase 5633  lep1t 5814  ledivp1t 5907  xrsupss 6080  xrinfmss 6081  zbtwnre 6223  fraclt1t 6233  fracge0t 6234  flhalft 6248  ceiget 6250  ceim1lt 6251  fldivt 6256  qbtwnre 6279  ser1add2 6339  ser1add 6340  uz11t 6433  fzneuzt 6519  expubndt 6609  reim0t 6775  absnegt 6832  abscjt 6834  sqabsaddt 6848  sqabssubt 6849  leabst 6864  cvg3 6923  faclbnd4lem3 6950  faclbnd4lem4 6951  bcn0t 6963  bcnnt 6964  fsum1ps 7018  fsumsplit 7020  binomlem5 7070  climconst2 7095  climrecl 7110  climge0 7112  isumcmpi 7215  efaddlem6 7343  efcant 7368  reeff1o 7426  resin4pt 7436  recos4pt 7437  sincossqt 7461  infpss 7575  tgvalt 7615  cctop 7649  cldval 7663  ntrfval 7664  clsfval 7665  cldcls 7679  cmclsopn 7690  neifval 7711  lpfval 7739  cncnplem4 7774  blfval 7832  ssblex 7853  opnfval 7854  tgioolem 7911  lmfval 7922  caufval 7923  lmuni 7948  opr1cn 7975  opr2cn 7976  bopcnlem2 7979  bcthlem16 8011  isgrpi 8039  grpidval 8054  grpinvfval 8062  grpinvid 8070  grpdivfval 8077  issubg 8112  cnaddabl 8122  vcz 8185  vcoprne 8194  nvz0 8292  sspz 8390  lno0 8413  0lno 8446  ipasslem2 8487  sincolem 8660  sinkpi 8692  abssinper 8707  shftefif1olem 8736  ococint 9292  spanvalt 9294  shunss 9332  pjocin 9638  nmcopexlem6 9951  lncnopbd 9961  nmcfnexlem6 9980  riesz3 9990  cnlnadjlem7 10001  hmopidmpj 10075  pjclem4 10122  pj3s 10130  hstoct 10144  hstnmoct 10145  hstoht 10154  hst0t 10155  mdsl2 10244  irredlem3 10314  irredlem4 10315  dmdbr5at 10344  ghomgrpilem2 10381  ghomid 10389  idhme 10508  hmphre 10516  sfvlim 10576  sfvlimOLD 10577  mslb1 10600  cnvtr 10609  imonclem 10712

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