Theorem orbi12d 690

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bi12d.1	|- (ph -> (ps <-> ch))
bi12d.2	|- (ph -> (th <-> ta))

Assertion

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

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	orbi1d 683	. 2 |- (ph -> ((ps \/ th) <-> (ch \/ th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	orbi2d 682	. 2 |- (ph -> ((ch \/ th) <-> (ch \/ ta)))
5	2, 4	bitrd 244	1 |- (ph -> ((ps \/ th) <-> (ch \/ ta)))

Syntax hints:   -> wi 4   <-> wb 176   \/ wo 357

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 177  df-or 359

This theorem is referenced by:  pm4.39  841  3orbi123d  1251  cadbi123d  1383  eueq3  3011  sbcor  3090  sbcorg  3091  elprg  3750  eltpg  3769  preq12bg  4128  nnc0suc  4412  nndisjeq  4429  lefinlteq  4463  evenodddisjlem1  4515  fununi  5160  funcnvuni  5161  fun11iun  5305  unpreima  5408  clos1basesuc  5882  clos1basesucg  5884  connexrd  5930  connexd  5931  qsdisj  5995  ncdisjeq  6148  nc0le1  6216  leconnnc  6218  muc0or  6252  nchoicelem9  6297  nchoicelem16  6304  nchoicelem17  6305  nchoice  6308