Theorem jaodan 783

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	|- ( ( ph /\ ps ) -> ch )
jaodan.2	|- ( ( ph /\ th ) -> ch )

Assertion

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

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 |- ( ( ph /\ ps ) -> ch )
2	1	ex 434	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 434	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 380	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 429	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

Syntax hints:   -> wi 4   \/ wo 368   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371

This theorem is referenced by:  mpjaodan  784  andi  862  ccase  937  mpjao3dan  1285  relop  5011  poltletr  5254  oeoa  7057  oeoe  7059  phplem3  7513  ssnnfi  7553  unwdomg  7820  numwdom  8250  infpssrlem5  8497  fin23lem24  8512  fin23lem28  8530  fin1a2lem10  8599  zornn0g  8695  gchdomtri  8817  fpwwe2lem12  8829  fpwwe2lem13  8830  msqgt0  9881  recextlem2  9988  lemul1a  10204  nnnn0addcl  10631  un0addcl  10634  un0mulcl  10635  elz2  10684  xaddnemnf  11225  xaddnepnf  11226  rexmul  11255  xlemul1a  11272  xrsupsslem  11290  xrinfmsslem  11291  ixxun  11337  fzsplit2  11495  fzsuc2  11535  elfzp12  11560  seqf1olem2  11867  expp1  11893  expneg  11894  expcllem  11897  mulexpz  11925  expaddz  11929  expmulz  11931  faclbnd4lem3  12092  faclbnd4lem4  12093  faclbnd4  12094  bcpasc  12118  wrdsymb0  12280  ccatass  12307  ccatswrd  12371  cats1un  12391  revccat  12427  summo  13215  sumss2  13224  fsumsplit  13237  geomulcvg  13357  ef0lem  13385  dvdseq  13601  odd2np1  13613  sadcaddlem  13674  gcdcllem3  13718  rpexp1i  13828  pcid  13960  4sqlem16  14042  funcres2c  14832  lubun  15314  mulgneg  15666  mulgnn0z  15668  frgpup3lem  16295  gsumzunsnd  16473  gsumunsnd  16474  dprddisj2  16559  dprddisj2OLD  16560  dmdprdsplit2  16567  dprdsplit  16569  gsumdixpOLD  16722  gsumdixp  16723  lssvs0or  17213  evlslem4OLD  17612  evlslem4  17613  txhaus  19242  xkoptsub  19249  ptunhmeo  19403  xpsxmetlem  19976  xpsmet  19979  mbfss  21146  itg1addlem2  21197  iblss2  21305  itgsplit  21335  limcres  21383  ftc1lem5  21534  coe1mul3  21593  dgrlt  21755  abelthlem3  21920  atanlogaddlem  22330  atanlogsub  22333  atans2  22348  efrlim  22385  bposlem2  22646  lgsdir2lem4  22687  2sqb  22739  pntpbnd1  22857  ostthlem1  22898  brbtwn2  23173  axcontlem2  23233  uvtx01vtx  23422  isoun  26019  mul2lt0bi  26064  eliccelico  26089  elicoelioo  26090  fzsplit3  26100  gsumunsnf  26267  xrge0iifhom  26389  esumsplit  26528  sibfinima  26747  subfacp1lem4  27093  subfacp1lem5  27094  fprodsplit  27498  bpoly2  28222  bpoly3  28223  ftc1cnnc  28492  ftc1anclem2  28494  eqfnun  28641  fdc  28667  incsequz2  28671  unichnidl  28857  rexzrexnn0  29168  pell14qrexpcl  29234  elpell1qr2  29239  acongeq  29352  jm2.23  29371  rpnnen3  29407  sumpair  29783  bnj1137  32082  lkrss2N  32910  cdlemg27b  34436  tendoex  34715  dihmeetlem2N  35040  dvh3dim3N  35190