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 756  dedlema 762  dedlemb 763  ax11indi 1367  psssstr 2150  opthpr 2483  sotric 2858  ordtr2 3000  trsucss 3054  ordunisuc2 3113  limom 3144  relop 3273  fununi 3561  tfrlem11 3919  oaass 4193  omordi 4195  om00 4204  odi 4208  oewordi 4216  omsmolem 4254  mapdom2 4488  nneneq 4506  suppr 4578  inf3lem6 4606  r1ord3 4645  rankxplim3 4702  zorn2lem7 4782  cardnn 4812  carddom 4824  sucdom 4830  unxpdomlem 4831  alephordi 4862  cardaleph 4873  alephval2 4890  cfsuc 4903  indpi 5022  ltrpq 5073  prub 5086  sqgt0sr 5203  ssgt0sr 5205  suppsr3 5212  lelttrt 5511  ltletrt 5512  letrt 5513  xrlttrit 5540  xrlelttrt 5550  xrltletrt 5551  xrletrt 5552  lemul1it 5808  lemul1itOLD 5809  squeeze0 5892  nnleltp1t 5922  nnsub 5924  sup2 6019  xrsupexmnf 6042  xrinfmexpnf 6043  supxrun 6053  lt0nnn0 6084  nnnn0addclt 6093  elnnz 6113  nn0subt 6129  monoord 6258  ioojoint 6376  elfzp1 6470  fsequb 6483  expp1t 6534  expeq0t 6545  expne0it 6548  expge0t 6551  expwordit 6563  sqlecant 6601  nn0opth 6626  sqrlem6 6638  sqrlem12 6644  seq1bnd 6868  facdivt 6900  facwordit 6902  faclbnd 6903  facavgt 6913  ser1cmp2 7135  expcnvlem6 7190  infxpidmlem7 7515  infcda 7524  infdif 7525  infxp 7529  0top 7592  bcthlem18 7973  nvmul0or 8229  pilem2 8629  hvmul0ort 8849  lnopcon 9918  lnfncon 9945  atcvat 10268  cdrci 10436

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