Theorem mpdan 768

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 402	. 2 |- (ph -> (ps -> ch))
4	1, 3	mpd 29	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mpancom 769  mpd3an3 1192  eueq2 2429  eueq3 2430  csbiegf 2575  csbnestglem 2580  csbidmg 2584  reuunisn 3822  onsucuni 3907  elrnopabg 4773  fnressn 4812  elrnoprabg 5066  oaordi 5227  oaabs 5309  dom2d 5463  canth2g 5549  php4 5610  onfin 5613  pwfilem 5660  pwfi 5661  supsnALT 5682  infeq5 5727  trcl 5752  oncardval 5865  cardonle 5868  infenomsub 5889  cardsucinf 5993  canth3 6002  cardaleph 6033  cfval 6054  reclem3pr 6310  reclem4pr 6311  0idsr 6358  lecasei 6804  lep1 6990  ledivp1 7088  xrsupss 7287  xrinfmss 7288  zbtwnre 7434  qbtwnre 7459  fraclt1 7470  fracge0 7471  flhalf 7487  ceige 7489  ceim1l 7490  fldiv 7497  uz11 7601  fzneuz 7697  cardfz 7719  ser1add2i 7751  ser1addi 7752  expubnd 7853  reim0 8024  absneg 8083  abscj 8085  sqabsadd 8099  sqabssub 8100  leabs 8115  cvg3i 8175  faclbnd4lem3 8202  faclbnd4lem4 8203  bcn0 8215  bcnn 8216  fsum1ps 8278  fsumsplit 8280  binomlem5 8330  climconst2 8355  climrecl 8370  climge0 8372  isumcmpii 8476  efaddlem6 8605  efcan 8630  reeff1o 8691  resin4p 8701  recos4p 8702  sincossq 8726  infpss 8843  tgval 8886  cctop 8922  cldval 8942  ntrfval 8943  clsfval 8944  cldcls 8958  cmclsopn 8969  neifval 8990  lpfval 9018  cncnplem4 9054  blfval 9112  ssblex 9133  opnfval 9134  tgioolem 9192  lmfval 9203  caufval 9204  lmuni 9229  opr1cn 9256  opr2cn 9257  bopcnlem2 9260  bcthlem16 9292  isgrpi 9322  grpinvfval 9350  grpinvid 9358  grpdivfval 9366  gxoprval 9380  gxid 9396  issubg 9425  cnaddabl 9434  ringlz 9487  ringrz 9488  vcz 9521  vcoprne 9530  nvz0 9628  sspz 9733  lno0 9756  0lno 9790  ipasslem2 9832  sincolem 10014  abssinper 10062  shftefif1olem 10095  oprabco 10159  fixp 10180  ghomid 10197  subspid 10249  fgf 10283  sfvlim 10296  cncomp 10331  on1el6 10414  ococin 10930  spanval 10932  shunssi 10970  pjocini 11278  nmcopexlem6 11593  lncnopbd 11603  nmcfnexlem6 11622  riesz3i 11632  cnlnadjlem7 11643  opsqrlem3 11713  hmopidmpji 11724  pjclem4 11772  pj3si 11780  hstoc 11794  hstnmoc 11795  hstoh 11804  hst0 11805  mdsl2i 11894  irredlem3 11964  irredlem4 11965  dmdbr5ati 11994  bnj1107 12923  bnj97 13220  bnj1006 13371  bnj1253 13470  bnj1281 13474  bnj1282 13475  bnj1283 13476  bnj1463 13550  bnj1312 13557  ghomgrpilem2 13629  iddvds 13668  1dvds 13669  dvdsadd 13688  eucalgval 13749  eucalg 13755  1idssfct 13770  wfrlem5 13961  bdayval 13989  sege 14595  gaplc 14731  curgrpact 14735  mulveczer 14822  svli2 14826  idhme 14879  hmphre 14884  cntrsetlem 14999  mslb1 15007  cnvtr 15016  dualcat2 15133  imonclem 15162  iepiclem 15172  carinttar2 15280  isline1 15294  infenomsubOLD 15398  compsublem 15430  2ndcctbss 15478  neibastop2lem4 15522  ufileu 15573  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  sfcls 15604  filclus 15605  tailf 15633  fnopabco 15711  firnfi 15741  fisup2g 15768  elfzp12 15795  rddif 15798  absrdbnd 15799  sdc 15811  fdc 15812  iocopnst 15877  lincmb01cmp 15878  lincmb01icc 15879  cncfres 15895  tlmval 15903  txcld 15914  cnopropabco 15917  cnoprab1 15921  cnoprab2 15922  totbndbnd 15944  heiborlem23 15977  heiborlem32 15986  heiborlem41 15995  reparpht 16065  pi1gp 16095  ringnegmn1l 16102  ringnegmn1r 16103  ringneglmul 16104  ringnegrmul 16105  iscringd 16147  idlnegcl 16170  0idl 16173  0ring 16175  keridl 16180  smprngpr 16200  latjcom 16860  latlej1 16861  latlej2 16862  latjle12 16863  latmcom 16870  latmle1 16871  latmle2 16872  lubun 16899  lubunNEW 16900  glb0 16920  opoc1 16929  grpidclNEW 17118  grpinvidNEW 17133  cnaddablNEW 17139  cnaddablxNEW 17140  zaddablxNEW 17141  ringidcl 17150  ringlzNEW 17156  ringrzNEW 17157  pmap0 17245  pmap1 17247  pol1 17323

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

Copyright terms: Public domain