Theorem orbi2d 466

Description: Deduction adding a left disjunct to both sides of a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	imbi2d 464	. 2 |- (ph -> ((-. th -> ps) <-> (-. th -> ch)))
3		df-or 197	. 2 |- ((th \/ ps) <-> (-. th -> ps))
4		df-or 197	. 2 |- ((th \/ ch) <-> (-. th -> ch))
5	2, 3, 4	3bitr4g 428	1 |- (ph -> ((th \/ ps) <-> (th \/ ch)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195

This theorem is referenced by:  orbi1d 467  orbi12d 475  orbidi 510  eueq2 1429  eueq3 1430  sbc2or 1454  ifeq2 1779  elsucg 2290  elsuc2g 2291  ordtri2or 2328  ltsopi 3810  suplem2pr 3956  mul0ort 4212  elznn0 4576  zltp1let 4597

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org