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

Syntax hints:   -> wi 4   \/ wo 366   /\ wa 367

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 368  df-an 369

This theorem is referenced by:  mpjaodan  784  andi  865  ccase  944  mpjao3dan  1293  relop  5066  poltletr  5312  oeoa  7164  oeoe  7166  phplem3  7617  ssnnfi  7655  unwdomg  7925  numwdom  8353  infpssrlem5  8600  fin23lem24  8615  fin23lem28  8633  fin1a2lem10  8702  zornn0g  8798  gchdomtri  8918  fpwwe2lem12  8930  fpwwe2lem13  8931  msqgt0  9990  recextlem2  10097  lemul1a  10313  nnnn0addcl  10743  un0addcl  10746  un0mulcl  10747  elz2  10798  xaddnemnf  11354  xaddnepnf  11355  rexmul  11384  xlemul1a  11401  xrsupsslem  11419  xrinfmsslem  11420  ixxun  11466  fzsplit2  11631  fzsuc2  11659  elfzp12  11679  seqf1olem2  12050  expp1  12076  expneg  12077  expcllem  12080  mulexpz  12109  expaddz  12113  expmulz  12115  faclbnd4lem3  12275  faclbnd4lem4  12276  faclbnd4  12277  bcpasc  12301  ccatass  12514  ccatrn  12515  ccatswrd  12592  cats1un  12612  revccat  12651  summo  13541  sumss2  13550  fsumsplit  13564  geomulcvg  13687  fprodsplit  13772  ef0lem  13816  dvdseq  14035  odd2np1  14048  sadcaddlem  14109  gcdcllem3  14153  rpexp1i  14264  pcid  14398  4sqlem16  14480  funcres2c  15307  lubun  15870  mulgneg  16277  mulgnn0z  16279  frgpup3lem  16912  gsumzunsnd  17096  gsumunsnfd  17097  dprddisj2  17200  dprddisj2OLD  17201  dmdprdsplit2  17208  dprdsplit  17210  gsumdixpOLD  17370  gsumdixp  17371  lssvs0or  17869  evlslem4OLD  18286  evlslem4  18287  refun0  20101  txhaus  20233  xkoptsub  20240  ptunhmeo  20394  xpsxmetlem  20967  xpsmet  20970  mbfss  22138  itg1addlem2  22189  iblss2  22297  itgsplit  22327  limcres  22375  ftc1lem5  22526  coe1mul3  22585  dgrlt  22748  abelthlem3  22913  atanlogaddlem  23360  atanlogsub  23363  atans2  23378  efrlim  23416  bposlem2  23677  lgsdir2lem4  23718  2sqb  23770  pntpbnd1  23888  ostthlem1  23929  hlbtwn  24115  brbtwn2  24329  axcontlem2  24389  uvtx01vtx  24613  isoun  27667  nn0sqeq1  27712  mul2lt0bi  27719  eliccelico  27741  elicoelioo  27742  fzsplit3  27752  xrge0iifhom  28073  esumsplit  28201  esumpad2  28204  sibfinima  28464  subfacp1lem4  28816  subfacp1lem5  28817  mclsax  29118  bpoly2  29972  bpoly3  29973  ftc1cnnc  30255  ftc1anclem2  30257  eqfnun  30378  fdc  30404  incsequz2  30408  unichnidl  30594  rexzrexnn0  30903  pell14qrexpcl  30968  elpell1qr2  30973  acongeq  31086  jm2.23  31104  rpnnen3  31140  radcnvrat  31363  dvdslcm  31372  lcmeq0  31374  lcmcl  31375  lcmneg  31377  lcmgcd  31381  sumpair  31577  cncfiooicclem1  31862  fourierdlem80  32135  fourierdlem93  32148  ccatpfx  32584  bnj1137  34398  lkrss2N  35307  cdlemg27b  36835  tendoex  37114  dihmeetlem2N  37439  dvh3dim3N  37589