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 338	. 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 220

This theorem is referenced by:  jaodan 426  jaao 427  pm2.63 429  ccased 761  dedlema 767  dedlemb 768  dn1 779  ax11indi 1406  psssstr 2204  opthpr 2550  sotric 2939  ordtr2 3019  trsucss 3057  ordunisuc2 3198  limom 3233  relop 3365  fununi 3668  tfrlem11 4222  oaass 4331  omordi 4333  om00 4342  odi 4346  oewordi 4354  omsmolem 4396  ac6sfilem3 4590  mapdom2 4641  nneneq 4659  suppr 4733  inf3lem6 4763  r1ord3 4803  rankxplim3 4860  zorn2lem7 4940  cardnn 4970  carddom 4985  sucdom 4992  unxpdomlem 4993  alephordi 5024  cardaleph 5035  alephval2 5052  cfsuc 5065  indpi 5188  ltrpq 5239  prub 5252  sqgt0sr 5369  ssgt0sr 5371  suppsr3 5378  lelttr 5677  ltletr 5678  letr 5679  xrlttri 5706  xrlelttr 5716  xrltletr 5717  xrletr 5718  lemul1a 5981  lemul1aOLD 5982  squeeze0 6069  nnleltp1 6100  nnsubi 6102  rpneg 6211  sup2 6219  xrsupexmnf 6242  xrinfmexpnf 6243  supxrun 6253  lt0nnn0 6284  nnnn0addcl 6293  elnnz 6313  nn0sub 6329  monoord 6482  ioojoin 6543  elfzp1 6641  fsequb 6654  expp1 6769  expeq0 6780  expge0 6785  expwordi 6800  sqlecan 6838  nn0opthi 6867  sqrlem6 6879  sqrlem12 6885  seq1bndi 7113  facdiv 7145  facwordi 7147  faclbnd 7148  facavg 7158  ser1cmp2i 7380  expcnvlem6 7436  infxpidmlem7 7770  infcda 7779  infdif 7780  infxp 7784  0top 7847  indistop 7860  bcthlem18 8227  gxnn0neg 8319  gxnn0suc 8320  gxneg 8322  gxsuc 8328  gxadd 8331  gxmul 8334  nvmul0or 8519  pilem2 8939  hvmul0or 9169  lnopconi 10242  lnfnconi 10269  atcvati 10595  cdrci 10994  finminlem 11418  fictb 11423  finsschain 11425  omsubsdom 11442  omsubdom 11443  omsubel 11444  omsublim 11448  infenomsub 11450  subntr 11482  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  dfcon2 11501  cnconn 11503  reconn 11512  refssfne 11565  comppfsc 11578  extbas1 11641  ufprim 11654  filssufillem 11655  filssufil 11656  ufilen 11664  filcon 11665  cnpfillim 11686  elfilmap 11690  tosdir 11755  indexf 11847  fzm1 11867  absz 11868  absmod0 11873  fsumlt1 11894  geomcau 11914  iccsplit 11919  heiborlem15 12025

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 145  df-or 222  df-an 223

Copyright terms: Public domain