Theorem jaod 426

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 428  jaao 429  pm2.63 430  ccased 758  dedlema 764  dedlemb 765  ax11indi 1369  psssstr 2155  opthpr 2489  sotric 2866  ordtr2 3008  trsucss 3062  ordunisuc2 3121  limom 3152  relop 3281  fununi 3569  tfrlem11 3927  oaass 4201  omordi 4203  om00 4212  odi 4216  oewordi 4224  omsmolem 4262  mapdom2 4500  nneneq 4518  suppr 4599  inf3lem6 4627  r1ord3 4667  rankxplim3 4724  zorn2lem7 4804  cardnn 4834  carddom 4846  sucdom 4852  sucdomOLD 4853  unxpdomlem 4854  alephordi 4885  cardaleph 4896  alephval2 4913  cfsuc 4927  indpi 5046  ltrpq 5097  prub 5110  sqgt0sr 5227  ssgt0sr 5229  suppsr3 5236  lelttrt 5535  ltletrt 5536  letrt 5537  xrlttrit 5564  xrlelttrt 5574  xrltletrt 5575  xrletrt 5576  lemul1it 5839  lemul1itOLD 5840  squeeze0 5926  nnleltp1t 5956  nnsub 5958  sup2 6053  xrsupexmnf 6076  xrinfmexpnf 6077  supxrun 6087  lt0nnn0 6118  nnnn0addclt 6127  elnnz 6147  nn0subt 6163  monoord 6295  ioojoint 6417  elfzp1 6511  fsequb 6524  expp1t 6575  expeq0t 6586  expne0it 6589  expge0t 6592  expwordit 6604  sqlecant 6642  nn0opth 6667  sqrlem6 6679  sqrlem12 6685  seq1bnd 6910  facdivt 6942  facwordit 6944  faclbnd 6945  facavgt 6955  ser1cmp2 7177  expcnvlem6 7232  infxpidmlem7 7559  infcda 7568  infdif 7569  infxp 7573  0top 7634  bcthlem18 8013  nvmul0or 8268  pilem2 8667  hvmul0ort 8889  lnopcon 9958  lnfncon 9985  atcvat 10308  cdrci 10480

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