MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaodan Unicode version

Theorem jaodan 760
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
StepHypRef Expression
1 jaodan.1 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
21ex 423 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 423 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
52, 4jaod 369 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
65imp 418 1  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358
This theorem is referenced by:  mpjaodan  761  andi  837  ccase  912  relop  4834  poltletr  5078  oeoa  6595  oeoe  6597  phplem3  7042  ssnnfi  7082  unwdomg  7298  numwdom  7686  infpssrlem5  7933  fin23lem24  7948  fin23lem28  7966  fin1a2lem10  8035  zornn0g  8132  gchdomtri  8251  fpwwe2lem12  8263  fpwwe2lem13  8264  msqgt0  9294  recextlem2  9399  lemul1a  9610  nnnn0addcl  9995  un0addcl  9997  un0mulcl  9998  elz2  10040  xaddnemnf  10561  xaddnepnf  10562  rexmul  10591  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  ixxun  10672  fzsplit2  10815  fzsuc2  10842  elfzp12  10861  seqf1olem2  11086  expp1  11110  expneg  11111  expcllem  11114  mulexpz  11142  expaddz  11146  expmulz  11148  faclbnd4lem3  11308  faclbnd4lem4  11309  faclbnd4  11310  bcpasc  11333  ccatass  11436  ccatswrd  11459  cats1un  11476  revccat  11484  summo  12190  sumss2  12199  fsumsplit  12212  geomulcvg  12332  ef0lem  12360  dvdseq  12576  odd2np1  12587  sadcaddlem  12648  gcdcllem3  12692  rpexp1i  12800  pcid  12925  4sqlem16  13007  funcres2c  13775  lubun  14227  mulgneg  14585  mulgnn0z  14587  frgpup3lem  15086  gsumunsn  15221  dprddisj2  15274  dmdprdsplit2  15281  dprdsplit  15283  gsumdixp  15392  lssvs0or  15863  evlslem4  16245  txhaus  17341  xkoptsub  17348  ptunhmeo  17499  xpsxmetlem  17943  xpsmet  17946  mbfss  19001  itg1addlem2  19052  iblss2  19160  itgsplit  19190  limcres  19236  ftc1lem5  19387  coe1mul3  19485  dgrlt  19647  abelthlem3  19809  atanlogaddlem  20209  atanlogsub  20212  atans2  20227  efrlim  20264  bposlem2  20524  lgsdir2lem4  20565  2sqb  20617  pntpbnd1  20735  ostthlem1  20776  fzsplit3  23031  isoun  23242  eliccelico  23270  elicoelioo  23271  xrge0iifhom  23319  esumsplit  23431  hasheuni  23453  measiuns  23544  subfacp1lem4  23714  subfacp1lem5  23715  brbtwn2  24533  axcontlem2  24593  bpoly2  24792  bpoly3  24793  eqfnun  26387  fdc  26455  incsequz2  26459  unichnidl  26656  rexzrexnn0  26885  pell14qrexpcl  26952  elpell1qr2  26957  acongeq  27070  jm2.23  27089  rpnnen3  27125  sumpair  27706  uvtx01vtx  28164  bnj1137  29025  lubunNEW  29163  lkrss2N  29359  cdlemg27b  30885  tendoex  31164  dihmeetlem2N  31489  dvh3dim3N  31639
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 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator