Theorem jaod 469

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		jaod.1	. 2 |- (ph -> (ps -> ch))
2		jaod.2	. 2 |- (ph -> (th -> ch))
3		jao 367	. 2 |- ((ps -> ch) -> ((th -> ch) -> ((ps \/ th) -> ch)))
4	1, 2, 3	sylc 83	1 |- (ph -> ((ps \/ th) -> ch))

Syntax hints:   -> wi 3   \/ wo 239

This theorem is referenced by:  jaodan 471  jaao 472  pm2.63 474  ecase3d 827  ccased 830  dedlema 837  dedlemaOLD 838  dedlemb 839  dedlembOLD 840  prlem1 848  dn1 855  dn1OLD 856  19.33b 1444  psssstr 2716  opthpr 3156  sotric 3615  ordtr2OLD 3709  trsuc2 3754  trsucss 3755  ordunisuc2 3926  limom 3967  relop 4113  fununi 4481  tfrlem11 5129  oaass 5243  omordi 5245  om00 5254  odi 5258  oewordi 5266  omsmolem 5313  ac6sfilem3 5508  mapdom2 5588  nneneq 5606  suppr 5680  inf3lem6 5724  r1ord3 5768  rankxplim3 5825  cardnn 5870  omsubsdom 5881  omsubdom 5882  omsubel 5883  omsublim 5887  infenomsub 5889  zorn2lem7 5956  carddom 5987  sucdom 5994  unxpdomlem 5995  alephordi 6022  cardaleph 6033  alephval2 6050  cfsuc 6063  indpi 6186  ltrpq 6237  prub 6250  sqgt0sr 6367  ssgt0sr 6369  suppsr3 6376  lelttr 6693  ltletr 6694  letr 6695  xrlttri 6727  xrlelttr 6737  xrltletr 6738  xrletr 6739  lemul1a 7019  lemul1aOLD 7020  squeeze0 7107  nnleltp1 7138  nnsubi 7140  rpneg 7252  sup2 7260  xrsupexmnf 7283  xrinfmexpnf 7284  supxrun 7294  lt0nnn0 7325  nnnn0addcl 7334  elnnz 7354  nn0sub 7370  monoord 7523  ioojoin 7585  elfzp1 7683  fsequb 7702  expp1 7817  expeq0 7828  expge0 7833  expwordi 7848  sqlecan 7887  sqrlem6 7928  sqrlem12 7934  seq1bndi 8162  facdiv 8194  facwordi 8196  faclbnd 8197  facavg 8207  ser1cmp2i 8437  expcnvlem6 8493  infxpidmlem7 8827  infcda 8836  infdif 8837  infxp 8841  0top 8905  indistop 8918  bcthlem18 9294  gxnn0neg 9386  gxnn0suc 9387  gxneg 9389  gxsuc 9395  gxadd 9398  gxmul 9401  nvmul0or 9604  pilem2 10021  indexfi 10174  cdrci 10182  extbas1 10291  elfilmap 10312  tosdir 10358  hvmul0or 10526  lnopconi 11600  lnfnconi 11627  atcvati 11958  absdvdsb 13673  dvdsabsb 13674  dvdsleabs 13694  mulgcdlem7 13762  trsuc2OLD 13793  untsucf 13798  dfon2lem6 13854  poxp 13949  soxp 13950  wfrlem14 13970  wfrlem15 13971  axdenselem4 14022  meran1 14235  finminlem 15367  fictb 15371  finsschain 15373  omsubsdomOLD 15390  omsubdomOLD 15391  omsubelOLD 15392  omsublimOLD 15396  infenomsubOLD 15398  subntr 15425  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  dfcon2 15442  cnconn 15444  reconn 15451  refssfne 15504  comppfsc 15517  ufprim 15569  filssufillem 15570  filssufil 15571  ufilen 15579  filcon 15580  cnpfillim 15589  indexfiOLD 15755  fzm1 15796  absz 15797  absmod0 15802  fdc 15812  fsumlt1 15831  geomcau 15849  iccsplit 15854  heiborlem15 15969  divrngidl 16176  erreft 16259  pltletr 16791  cvrnbtwn4 16996  cvrat 17062  elpaddn0 17261  paddasslem17 17297  paddidm 17302  pmapjoin 17313

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-or 241  df-an 242

Copyright terms: Public domain