Theorem orcomd 403

Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)

Hypothesis

Ref	Expression
orcomd.1	|- ( ph -> ( ps \/ ch ) )

Assertion

Ref	Expression
orcomd	|- ( ph -> ( ch \/ ps ) )

Proof of Theorem orcomd

Step	Hyp	Ref	Expression
1		orcomd.1	. 2 |- ( ph -> ( ps \/ ch ) )
2		orcom 402	. 2 |- ( ( ps \/ ch ) <-> ( ch \/ ps ) )
3	1, 2	sylib 208	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  olcd  408  19.33b  1813  swopo  5045  fr2nr  5092  ordtri1  5756  ordequn  5828  ssonprc  6992  ordunpr  7026  ordunisuc2  7044  2oconcl  7583  erdisj  7794  ordtypelem7  8429  ackbij1lem18  9059  fin23lem19  9158  gchi  9446  inar1  9597  inatsk  9600  avgle  11274  nnm1nn0  11334  uzsplit  12412  fzospliti  12500  fzouzsplit  12503  fz1f1o  14441  odcl  17955  gexcl  17995  lssvs0or  19110  lspdisj  19125  lspsncv0  19146  mdetralt  20414  filconn  21687  limccnp  23655  dgrlt  24022  logreclem  24500  atans2  24658  basellem3  24809  sqff1o  24908  tgcgrsub2  25490  legov3  25493  colline  25544  tglowdim2ln  25546  mirbtwnhl  25575  colmid  25583  symquadlem  25584  midexlem  25587  ragperp  25612  colperp  25621  midex  25629  oppperpex  25645  hlpasch  25648  colopp  25661  colhp  25662  lmieu  25676  lmicom  25680  lmimid  25686  lmiisolem  25688  trgcopy  25696  cgracgr  25710  cgraswap  25712  cgracol  25719  hashecclwwlksn1  26954  znsqcld  29512  xlt2addrd  29523  fprodex01  29571  esumcvgre  30153  eulerpartlemgvv  30438  ordtoplem  32434  ordcmp  32446  onsucuni3  33215  dvasin  33496  unitresr  33885  lkrshp4  34395  2at0mat0  34811  trlator0  35458  dia2dimlem2  36354  dia2dimlem3  36355  dochkrshp  36675  dochkrshp4  36678  lcfl6  36789  lclkrlem2k  36806  hdmap14lem6  37165  hgmapval0  37184  acongneg2  37544  unxpwdom3  37665  elunnel2  39198  disjinfi  39380  xrssre  39564  icccncfext  40100  wallispilem3  40284  fourierdlem93  40416  fourierdlem101  40424  nneop  42320