Theorem orbi2d 737

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

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

Assertion

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

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		orbid.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 142	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	orim2d 735	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 156	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 735	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 127	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 103   \/ wo 662

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1d  738  orbi12d  740  dn1dc  902  xorbi2d  1312  eueq2dc  2774  r19.44mv  3352  rexprg  3462  rextpg  3464  swopolem  4088  sowlin  4103  elsucg  4187  elsuc2g  4188  ordsoexmid  4333  poleloe  4774  isosolem  5514  freceq2  6062  brdifun  6220  pitric  6625  elinp  6778  prloc  6795  ltexprlemloc  6911  ltsosr  7055  aptisr  7069  axpre-ltwlin  7163  gt0add  7792  apreap  7806  apreim  7822  elznn0  8499  elznn  8500  peano2z  8520  zindd  8598  elfzp1  9217  fzm1  9245  fzosplitsni  9373  cjap  9994  dvdslelemd  10451  zeo5  10495  lcmval  10652  lcmneg  10663  lcmass  10674  isprm6  10733  bj-nn0sucALT  11040