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

Theorem olcd 383
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 21711. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
orcd.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
olcd  |-  ( ph  ->  ( ch  \/  ps ) )

Proof of Theorem olcd
StepHypRef Expression
1 orcd.1 . . 3  |-  ( ph  ->  ps )
21orcd 382 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 378 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  pm2.48  390  pm2.49  391  orim12i  503  pm1.5  509  somin1  5270  soxp  6459  fowdom  7539  unxpwdom2  7556  fin1a2lem11  8290  axdc3lem2  8331  gchdomtri  8504  hargch  8552  alephgch  8553  nn1m1nn  10020  nnnegz  10285  rpneg  10641  ltpnf  10721  mnflt  10722  xrlttri  10732  xmulpnf1  10853  iccsplit  11029  elfznelfzo  11192  bc0k  11602  bcpasc  11612  hashv01gt1  11629  hashtpg  11691  hashf1  11706  fsum  12514  fsumsplit  12533  fsumdvds  12893  sumhash  13265  4sqlem17  13329  vdwlem6  13354  ram0  13390  mreexfidimd  13875  gsummulg  15537  drngnidl  16300  cnsubrg  16759  en2top  17050  fctop  17068  cctop  17070  metusttoOLD  18587  metustto  18588  pmltpclem2  19346  itg1addlem5  19592  itg10a  19602  dvne0  19895  plyeq0lem  20129  plymullem1  20133  aalioulem4  20252  aalioulem5  20253  aaliou2b  20258  ang180lem3  20653  basellem2  20864  musumsum  20977  dchrhash  21055  lgsdir2lem5  21111  rpvmasumlem  21181  rpvmasum2  21206  pntlemj  21297  eupath2lem2  21700  ex-natded5.7  21719  ex-natded5.13  21723  ex-natded9.20  21725  ex-natded9.20-2  21726  esumsn  24456  meascnbl  24573  sibfof  24654  fprod  25267  binomfallfaclem2  25356  sltres  25619  nobndup  25655  dfrdg4  25795  outsideoftr  26063  lineunray  26081  ftc1anclem3  26282  dvreasin  26290  areacirclem4  26295  smprngopr  26662  pell1234qrdich  26924  acongtr  27043  acongrep  27045  jm2.23  27067  jm2.25  27070  fnwe2lem3  27127  kelac2lem  27139  psgnunilem1  27393  psgnunilem5  27394  refsum2cnlem1  27684  fmul01lt1lem1  27690  wallispilem3  27792  2reu4a  27943  otsndisj  28065  otiunsndisj  28066  otiunsndisjX  28067  wrdsymb0  28170  ccatsymb  28179  cshwssizelem2  28281  cshwsdisj  28285  frgra2v  28389  3vfriswmgralem  28394  frgrawopreg  28438  2spotdisj  28450  2spotiundisj  28451  2spotmdisj  28457  lkrshpor  29905  cdleme22b  31138  tendoex  31772  lcfrlem9  32348
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
  Copyright terms: Public domain W3C validator