Theorem jaodan 785

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  786  andi  867  ccase  946  mpjao3dan  1296  relop  5143  poltletr  5392  oeoa  7248  oeoe  7250  phplem3  7700  ssnnfi  7741  unwdomg  8013  numwdom  8443  infpssrlem5  8690  fin23lem24  8705  fin23lem28  8723  fin1a2lem10  8792  zornn0g  8888  gchdomtri  9010  fpwwe2lem12  9022  fpwwe2lem13  9023  msqgt0  10080  recextlem2  10187  lemul1a  10403  nnnn0addcl  10833  un0addcl  10836  un0mulcl  10837  elz2  10888  xaddnemnf  11443  xaddnepnf  11444  rexmul  11473  xlemul1a  11490  xrsupsslem  11508  xrinfmsslem  11509  ixxun  11555  fzsplit2  11720  fzsuc2  11747  elfzp12  11767  seqf1olem2  12128  expp1  12154  expneg  12155  expcllem  12158  mulexpz  12187  expaddz  12191  expmulz  12193  faclbnd4lem3  12354  faclbnd4lem4  12355  faclbnd4  12356  bcpasc  12380  wrdsymb0  12556  ccatass  12586  ccatrn  12587  ccatswrd  12662  cats1un  12682  revccat  12721  summo  13520  sumss2  13529  fsumsplit  13543  geomulcvg  13666  fprodsplit  13751  ef0lem  13795  dvdseq  14014  odd2np1  14027  sadcaddlem  14088  gcdcllem3  14132  rpexp1i  14243  pcid  14377  4sqlem16  14459  funcres2c  15248  lubun  15731  mulgneg  16138  mulgnn0z  16140  frgpup3lem  16773  gsumzunsnd  16960  gsumunsnfd  16961  dprddisj2  17065  dprddisj2OLD  17066  dmdprdsplit2  17073  dprdsplit  17075  gsumdixpOLD  17235  gsumdixp  17236  lssvs0or  17734  evlslem4OLD  18151  evlslem4  18152  refun0  19993  txhaus  20125  xkoptsub  20132  ptunhmeo  20286  xpsxmetlem  20859  xpsmet  20862  mbfss  22030  itg1addlem2  22081  iblss2  22189  itgsplit  22219  limcres  22267  ftc1lem5  22418  coe1mul3  22477  dgrlt  22639  abelthlem3  22804  atanlogaddlem  23220  atanlogsub  23223  atans2  23238  efrlim  23275  bposlem2  23536  lgsdir2lem4  23577  2sqb  23629  pntpbnd1  23747  ostthlem1  23788  hlbtwn  23971  brbtwn2  24184  axcontlem2  24244  uvtx01vtx  24468  isoun  27496  nn0sqeq1  27538  mul2lt0bi  27545  eliccelico  27564  elicoelioo  27565  fzsplit3  27575  xrge0iifhom  27896  esumsplit  28040  sibfinima  28258  subfacp1lem4  28604  subfacp1lem5  28605  mclsax  28906  bpoly2  29794  bpoly3  29795  ftc1cnnc  30064  ftc1anclem2  30066  eqfnun  30187  fdc  30213  incsequz2  30217  unichnidl  30403  rexzrexnn0  30712  pell14qrexpcl  30778  elpell1qr2  30783  acongeq  30896  jm2.23  30913  rpnnen3  30949  radcnvrat  31171  dvdslcm  31180  lcmeq0  31182  lcmcl  31183  lcmneg  31185  lcmgcd  31189  sumpair  31364  cncfiooicclem1  31603  fourierdlem80  31858  fourierdlem93  31871  bnj1137  33784  lkrss2N  34634  cdlemg27b  36162  tendoex  36441  dihmeetlem2N  36766  dvh3dim3N  36916