Theorem jaod 424

Description: Deduction disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaod.1	|- (ph -> (ps -> ch))
jaod.2	|- (ph -> (th -> ch))

Assertion

Ref	Expression
jaod	|- (ph -> ((ps \/ th) -> ch))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jao 340	. 2 |- ((ps -> ch) -> ((th -> ch) -> ((ps \/ th) -> ch)))
2		jaod.1	. 2 |- (ph -> (ps -> ch))
3		jaod.2	. 2 |- (ph -> (th -> ch))
4	1, 2, 3	sylc 68	1 |- (ph -> ((ps \/ th) -> ch))

Syntax hints:   -> wi 3   \/ wo 222

This theorem is referenced by:  jaodan 426  jaao 427  pm2.63 428  ccased 754  dedlema 760  dedlemb 761  ax11indi 1360  psssstr 2142  opthpr 2476  sotric 2851  ordtr2 2992  trsucss 3046  ordunisuc2 3105  limom 3136  relop 3265  fununi 3549  tfrlem11 3906  oaass 4179  omordi 4181  om00 4190  odi 4194  oewordi 4202  omsmolem 4240  mapdom2 4474  nneneq 4492  suppr 4562  inf3lem6 4590  r1ord3 4629  rankxplim3 4686  zorn2lem7 4766  cardnn 4796  carddom 4808  sucdom 4814  unxpdomlem 4815  alephordi 4846  cardaleph 4857  alephval2 4874  cfsuc 4887  indpi 5006  ltrpq 5057  prub 5070  sqgt0sr 5187  ssgt0sr 5189  suppsr3 5196  lelttrt 5496  ltletrt 5497  letrt 5498  xrlttrit 5525  xrlelttrt 5535  xrltletrt 5536  xrletrt 5537  lemul1it 5793  lemul1itOLD 5794  squeeze0 5872  nnleltp1t 5901  nnsub 5903  sup2 5998  xrsupexmnf 6021  xrinfmexpnf 6022  supxrun 6032  lt0nnn0 6063  nnnn0addclt 6072  elnnz 6092  nn0subt 6108  monoord 6231  elfzp1 6442  fsequb 6455  expp1t 6506  expeq0t 6517  expne0it 6519  expge0t 6522  expwordit 6534  sqlecant 6572  nn0opth 6596  sqrlem6 6608  sqrlem12 6614  seq1bnd 6847  facdivt 6879  facwordit 6881  faclbnd 6882  facavgt 6892  ser1cmp2 7113  expcnvlem6 7167  infxpidmlem7 7501  infcda 7510  infdif 7511  infxp 7515  0top 7577  bcthlem18 7950  nvmul0or 8212  pilem2 8591  hvmul0ort 8815  lnopcon 9878  lnfncon 9905  atcvat 10221  cdrci 10381

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-or 224  df-an 225

Copyright terms: Public domain