Theorem jaodan 776

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  777  andi  855  ccase  930  mpjao3dan  1278  relop  4977  poltletr  5221  oeoa  7024  oeoe  7026  phplem3  7480  ssnnfi  7520  unwdomg  7787  numwdom  8217  infpssrlem5  8464  fin23lem24  8479  fin23lem28  8497  fin1a2lem10  8566  zornn0g  8662  gchdomtri  8784  fpwwe2lem12  8796  fpwwe2lem13  8797  msqgt0  9848  recextlem2  9955  lemul1a  10171  nnnn0addcl  10598  un0addcl  10601  un0mulcl  10602  elz2  10651  xaddnemnf  11192  xaddnepnf  11193  rexmul  11222  xlemul1a  11239  xrsupsslem  11257  xrinfmsslem  11258  ixxun  11304  fzsplit2  11461  fzsuc2  11499  elfzp12  11523  seqf1olem2  11830  expp1  11856  expneg  11857  expcllem  11860  mulexpz  11888  expaddz  11892  expmulz  11894  faclbnd4lem3  12055  faclbnd4lem4  12056  faclbnd4  12057  bcpasc  12081  wrdsymb0  12243  ccatass  12270  ccatswrd  12334  cats1un  12354  revccat  12390  summo  13178  sumss2  13187  fsumsplit  13200  geomulcvg  13319  ef0lem  13347  dvdseq  13563  odd2np1  13575  sadcaddlem  13636  gcdcllem3  13680  rpexp1i  13790  pcid  13922  4sqlem16  14004  funcres2c  14794  lubun  15276  mulgneg  15625  mulgnn0z  15627  frgpup3lem  16254  gsumunsnd  16427  dprddisj2  16511  dprddisj2OLD  16512  dmdprdsplit2  16519  dprdsplit  16521  gsumdixpOLD  16635  gsumdixp  16636  lssvs0or  17113  evlslem4OLD  17518  evlslem4  17519  txhaus  19062  xkoptsub  19069  ptunhmeo  19223  xpsxmetlem  19796  xpsmet  19799  mbfss  20966  itg1addlem2  21017  iblss2  21125  itgsplit  21155  limcres  21203  ftc1lem5  21354  coe1mul3  21456  dgrlt  21618  abelthlem3  21783  atanlogaddlem  22193  atanlogsub  22196  atans2  22211  efrlim  22248  bposlem2  22509  lgsdir2lem4  22550  2sqb  22602  pntpbnd1  22720  ostthlem1  22761  brbtwn2  22974  axcontlem2  23034  uvtx01vtx  23223  isoun  25821  mul2lt0bi  25867  eliccelico  25890  elicoelioo  25891  fzsplit3  25901  gsumunsnf  26097  xrge0iifhom  26221  esumsplit  26360  sibfinima  26573  subfacp1lem4  26919  subfacp1lem5  26920  fprodsplit  27323  bpoly2  28047  bpoly3  28048  ftc1cnnc  28310  ftc1anclem2  28312  eqfnun  28459  fdc  28485  incsequz2  28489  unichnidl  28675  rexzrexnn0  28987  pell14qrexpcl  29053  elpell1qr2  29058  acongeq  29171  jm2.23  29190  rpnnen3  29226  sumpair  29602  bnj1137  31688  lkrss2N  32387  cdlemg27b  33913  tendoex  34192  dihmeetlem2N  34517  dvh3dim3N  34667