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

Theorem jaodan 761
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 424 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 424 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
52, 4jaod 370 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
65imp 419 1  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359
This theorem is referenced by:  mpjaodan  762  andi  838  ccase  913  relop  5023  poltletr  5269  oeoa  6840  oeoe  6842  phplem3  7288  ssnnfi  7328  unwdomg  7552  numwdom  7940  infpssrlem5  8187  fin23lem24  8202  fin23lem28  8220  fin1a2lem10  8289  zornn0g  8385  gchdomtri  8504  fpwwe2lem12  8516  fpwwe2lem13  8517  msqgt0  9548  recextlem2  9653  lemul1a  9864  nnnn0addcl  10251  un0addcl  10253  un0mulcl  10254  elz2  10298  xaddnemnf  10820  xaddnepnf  10821  rexmul  10850  xlemul1a  10867  xrsupsslem  10885  xrinfmsslem  10886  ixxun  10932  fzsplit2  11076  fzsuc2  11104  elfzp12  11126  seqf1olem2  11363  expp1  11388  expneg  11389  expcllem  11392  mulexpz  11420  expaddz  11424  expmulz  11426  faclbnd4lem3  11586  faclbnd4lem4  11587  faclbnd4  11588  bcpasc  11612  ccatass  11750  ccatswrd  11773  cats1un  11790  revccat  11798  summo  12511  sumss2  12520  fsumsplit  12533  geomulcvg  12653  ef0lem  12681  dvdseq  12897  odd2np1  12908  sadcaddlem  12969  gcdcllem3  13013  rpexp1i  13121  pcid  13246  4sqlem16  13328  funcres2c  14098  lubun  14550  mulgneg  14908  mulgnn0z  14910  frgpup3lem  15409  gsumunsn  15544  dprddisj2  15597  dmdprdsplit2  15604  dprdsplit  15606  gsumdixp  15715  lssvs0or  16182  evlslem4  16564  txhaus  17679  xkoptsub  17686  ptunhmeo  17840  xpsxmetlem  18409  xpsmet  18412  mbfss  19538  itg1addlem2  19589  iblss2  19697  itgsplit  19727  limcres  19773  ftc1lem5  19924  coe1mul3  20022  dgrlt  20184  abelthlem3  20349  atanlogaddlem  20753  atanlogsub  20756  atans2  20771  efrlim  20808  bposlem2  21069  lgsdir2lem4  21110  2sqb  21162  pntpbnd1  21280  ostthlem1  21321  uvtx01vtx  21501  isoun  24089  eliccelico  24140  elicoelioo  24141  fzsplit3  24150  xrge0iifhom  24323  esumsplit  24447  sibfof  24654  subfacp1lem4  24869  subfacp1lem5  24870  fprodsplit  25289  brbtwn2  25844  axcontlem2  25904  bpoly2  26103  bpoly3  26104  ftc1cnnc  26279  ftc1anclem2  26281  eqfnun  26423  fdc  26449  incsequz2  26453  unichnidl  26641  rexzrexnn0  26864  pell14qrexpcl  26930  elpell1qr2  26935  acongeq  27048  jm2.23  27067  rpnnen3  27103  sumpair  27682  wrdsymb0  28170  bnj1137  29364  lubunNEW  29771  lkrss2N  29967  cdlemg27b  31493  tendoex  31772  dihmeetlem2N  32097  dvh3dim3N  32247
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator