Theorem orbi1d 739

Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
bid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
orbi1d	|- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )

Proof of Theorem orbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	orbi2d 738	. 2 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )
3		orcom 402	. 2 |- ( ( ps \/ th ) <-> ( th \/ ps ) )
4		orcom 402	. 2 |- ( ( ch \/ th ) <-> ( th \/ ch ) )
5	2, 3, 4	3bitr4g 303	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ 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:  orbi1  742  orbi12d  746  eueq2  3380  uneq1  3760  r19.45zv  4068  rexprg  4235  rextpg  4237  swopolem  5044  ordsseleq  5752  ordtri3  5759  infltoreq  8408  cantnflem1  8586  axgroth2  9647  axgroth3  9653  lelttric  10144  ltxr  11949  xmulneg1  12099  fzpr  12396  elfzp12  12419  caubnd  14098  lcmval  15305  lcmass  15327  isprm6  15426  vdwlem10  15694  irredmul  18709  domneq0  19297  opsrval  19474  znfld  19909  logreclem  24500  perfectlem2  24955  legov3  25493  lnhl  25510  colperpex  25625  lmif  25677  islmib  25679  friendshipgt3  27256  h1datom  28441  xrlelttric  29517  tlt3  29665  esumpcvgval  30140  sibfof  30402  segcon2  32212  poimirlem25  33434  cnambfre  33458  pridl  33836  ismaxidl  33839  ispridlc  33869  pridlc  33870  dmnnzd  33874  4atlem3a  34883  pmapjoin  35138  lcfl3  36783  lcfl4N  36784  sbc3orgOLD  38742  fourierdlem80  40403  el1fzopredsuc  41335  perfectALTVlem2  41631  nnsum3primesle9  41682  lindslinindsimp2  42252