Theorem jaodan 793

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

Syntax hints:   -> wi 4   \/ wo 370   /\ wa 371

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 189  df-or 372  df-an 373

This theorem is referenced by:  mpjaodan  794  andi  877  ccase  956  mpjao3dan  1334  elpreqpr  4160  relop  4984  poltletr  5231  oeoa  7295  oeoe  7297  phplem3  7750  ssnnfi  7788  unwdomg  8096  numwdom  8487  infpssrlem5  8734  fin23lem24  8749  fin23lem28  8767  fin1a2lem10  8836  zornn0g  8932  gchdomtri  9051  fpwwe2lem12  9063  fpwwe2lem13  9064  msqgt0  10131  recextlem2  10240  lemul1a  10456  nnnn0addcl  10897  un0addcl  10900  un0mulcl  10901  elz2  10951  mul2lt0bi  11399  xaddnemnf  11524  xaddnepnf  11525  rexmul  11554  xlemul1a  11571  xrsupsslem  11589  xrinfmsslem  11590  ixxun  11648  fzsplit2  11821  fzsuc2  11850  elfzp12  11870  seqf1olem2  12250  expp1  12276  expneg  12277  expcllem  12280  mulexpz  12309  expaddz  12313  expmulz  12315  faclbnd4lem3  12477  faclbnd4lem4  12478  faclbnd4  12479  bcpasc  12503  ccatass  12729  ccatrn  12730  ccatswrd  12807  cats1un  12827  revccat  12866  summo  13776  sumss2  13785  fsumsplit  13799  geomulcvg  13925  fprodsplit  14013  bpoly2  14103  bpoly3  14104  ef0lem  14126  dvdseq  14345  odd2np1  14358  sadcaddlem  14424  gcdcllem3  14468  dvdslcm  14556  lcmeq0  14558  lcmcl  14559  lcmneg  14561  lcmgcd  14565  rpexp1i  14666  pcid  14815  4sqlem16OLD  14897  4sqlem16  14903  funcres2c  15799  lubun  16362  mulgneg  16769  mulgnn0z  16771  frgpup3lem  17420  gsumzunsnd  17581  gsumunsnfd  17582  dprddisj2  17665  dmdprdsplit2  17672  dprdsplit  17674  gsumdixp  17830  lssvs0or  18326  evlslem4  18724  refun0  20523  txhaus  20655  xkoptsub  20662  ptunhmeo  20816  xpsxmetlem  21387  xpsmet  21390  mbfss  22595  itg1addlem2  22648  iblss2  22756  itgsplit  22786  limcres  22834  ftc1lem5  22985  coe1mul3  23041  dgrlt  23213  abelthlem3  23381  atanlogaddlem  23832  atanlogsub  23835  atans2  23850  efrlim  23888  bposlem2  24206  lgsdir2lem4  24247  2sqb  24299  pntpbnd1  24417  ostthlem1  24458  hlbtwn  24649  cgracol  24862  inaghl  24874  brbtwn2  24928  axcontlem2  24988  uvtx01vtx  25213  isoun  28275  nn0sqeq1  28317  eliccelico  28352  elicoelioo  28353  fzsplit3  28363  xrge0iifhom  28736  esumsplit  28867  esumpad2  28870  sibfinima  29165  bnj1137  29797  subfacp1lem4  29899  subfacp1lem5  29900  mclsax  30200  poimirlem2  31935  poimirlem8  31941  poimirlem22  31955  poimirlem28  31961  ftc1cnnc  32009  ftc1anclem2  32011  eqfnun  32041  fdc  32067  incsequz2  32071  unichnidl  32257  lkrss2N  32729  cdlemg27b  34257  tendoex  34536  dihmeetlem2N  34861  dvh3dim3N  35011  rexzrexnn0  35641  pell14qrexpcl  35707  elpell1qr2  35712  acongeq  35827  jm2.23  35845  rpnnen3  35881  radcnvrat  36657  sumpair  37350  cncfiooicclem1  37765  fourierdlem80  38044  fourierdlem93  38057  ccatpfx  38944