Theorem jaodan 761

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 424	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 424	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 370	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 419	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

Syntax hints:   -> wi 4   \/ wo 358   /\ wa 359

This theorem is referenced by:  mpjaodan  762  andi  838  ccase  913  relop  4982  poltletr  5228  oeoa  6799  oeoe  6801  phplem3  7247  ssnnfi  7287  unwdomg  7508  numwdom  7896  infpssrlem5  8143  fin23lem24  8158  fin23lem28  8176  fin1a2lem10  8245  zornn0g  8341  gchdomtri  8460  fpwwe2lem12  8472  fpwwe2lem13  8473  msqgt0  9504  recextlem2  9609  lemul1a  9820  nnnn0addcl  10207  un0addcl  10209  un0mulcl  10210  elz2  10254  xaddnemnf  10776  xaddnepnf  10777  rexmul  10806  xlemul1a  10823  xrsupsslem  10841  xrinfmsslem  10842  ixxun  10888  fzsplit2  11032  fzsuc2  11060  elfzp12  11081  seqf1olem2  11318  expp1  11343  expneg  11344  expcllem  11347  mulexpz  11375  expaddz  11379  expmulz  11381  faclbnd4lem3  11541  faclbnd4lem4  11542  faclbnd4  11543  bcpasc  11567  ccatass  11705  ccatswrd  11728  cats1un  11745  revccat  11753  summo  12466  sumss2  12475  fsumsplit  12488  geomulcvg  12608  ef0lem  12636  dvdseq  12852  odd2np1  12863  sadcaddlem  12924  gcdcllem3  12968  rpexp1i  13076  pcid  13201  4sqlem16  13283  funcres2c  14053  lubun  14505  mulgneg  14863  mulgnn0z  14865  frgpup3lem  15364  gsumunsn  15499  dprddisj2  15552  dmdprdsplit2  15559  dprdsplit  15561  gsumdixp  15670  lssvs0or  16137  evlslem4  16519  txhaus  17632  xkoptsub  17639  ptunhmeo  17793  xpsxmetlem  18362  xpsmet  18365  mbfss  19491  itg1addlem2  19542  iblss2  19650  itgsplit  19680  limcres  19726  ftc1lem5  19877  coe1mul3  19975  dgrlt  20137  abelthlem3  20302  atanlogaddlem  20706  atanlogsub  20709  atans2  20724  efrlim  20761  bposlem2  21022  lgsdir2lem4  21063  2sqb  21115  pntpbnd1  21233  ostthlem1  21274  uvtx01vtx  21454  isoun  24042  eliccelico  24093  elicoelioo  24094  fzsplit3  24103  xrge0iifhom  24276  esumsplit  24400  sibfof  24607  subfacp1lem4  24822  subfacp1lem5  24823  fprodsplit  25242  brbtwn2  25748  axcontlem2  25808  bpoly2  26007  bpoly3  26008  ftc1cnnc  26178  eqfnun  26313  fdc  26339  incsequz2  26343  unichnidl  26531  rexzrexnn0  26754  pell14qrexpcl  26820  elpell1qr2  26825  acongeq  26938  jm2.23  26957  rpnnen3  26993  sumpair  27573  bnj1137  29070  lubunNEW  29456  lkrss2N  29652  cdlemg27b  31178  tendoex  31457  dihmeetlem2N  31782  dvh3dim3N  31932

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

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361