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  4850  poltletr  5094  oeoa  6611  oeoe  6613  phplem3  7058  ssnnfi  7098  unwdomg  7314  numwdom  7702  infpssrlem5  7949  fin23lem24  7964  fin23lem28  7982  fin1a2lem10  8051  zornn0g  8148  gchdomtri  8267  fpwwe2lem12  8279  fpwwe2lem13  8280  msqgt0  9310  recextlem2  9415  lemul1a  9626  nnnn0addcl  10011  un0addcl  10013  un0mulcl  10014  elz2  10056  xaddnemnf  10577  xaddnepnf  10578  rexmul  10607  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  ixxun  10688  fzsplit2  10831  fzsuc2  10858  elfzp12  10877  seqf1olem2  11102  expp1  11126  expneg  11127  expcllem  11130  mulexpz  11158  expaddz  11162  expmulz  11164  faclbnd4lem3  11324  faclbnd4lem4  11325  faclbnd4  11326  bcpasc  11349  ccatass  11452  ccatswrd  11475  cats1un  11492  revccat  11500  summo  12206  sumss2  12215  fsumsplit  12228  geomulcvg  12348  ef0lem  12376  dvdseq  12592  odd2np1  12603  sadcaddlem  12664  gcdcllem3  12708  rpexp1i  12816  pcid  12941  4sqlem16  13023  funcres2c  13791  lubun  14243  mulgneg  14601  mulgnn0z  14603  frgpup3lem  15102  gsumunsn  15237  dprddisj2  15290  dmdprdsplit2  15297  dprdsplit  15299  gsumdixp  15408  lssvs0or  15879  evlslem4  16261  txhaus  17357  xkoptsub  17364  ptunhmeo  17515  xpsxmetlem  17959  xpsmet  17962  mbfss  19017  itg1addlem2  19068  iblss2  19176  itgsplit  19206  limcres  19252  ftc1lem5  19403  coe1mul3  19501  dgrlt  19663  abelthlem3  19825  atanlogaddlem  20225  atanlogsub  20228  atans2  20243  efrlim  20280  bposlem2  20540  lgsdir2lem4  20581  2sqb  20633  pntpbnd1  20751  ostthlem1  20792  fzsplit3  23047  isoun  23257  eliccelico  23285  elicoelioo  23286  xrge0iifhom  23334  esumsplit  23446  hasheuni  23468  measiuns  23559  subfacp1lem4  23729  subfacp1lem5  23730  brbtwn2  24605  axcontlem2  24665  bpoly2  24864  bpoly3  24865  ftc1cnnc  25025  eqfnun  26490  fdc  26558  incsequz2  26562  unichnidl  26759  rexzrexnn0  26988  pell14qrexpcl  27055  elpell1qr2  27060  acongeq  27173  jm2.23  27192  rpnnen3  27228  sumpair  27809  uvtx01vtx  28305  bnj1137  29341  lubunNEW  29785  lkrss2N  29981  cdlemg27b  31507  tendoex  31786  dihmeetlem2N  32111  dvh3dim3N  32261
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