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-mp 5  ax-1 6  ax-2 7  ax-3 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  3012  sbcor  3091  sbcorg  3092  elprg  3751  eltpg  3770  preq12bg  4129  nnc0suc  4413  nndisjeq  4430  lefinlteq  4464  evenodddisjlem1  4516  fununi  5161  funcnvuni  5162  fun11iun  5306  unpreima  5409  clos1basesuc  5883  clos1basesucg  5885  connexrd  5931  connexd  5932  qsdisj  5996  ncdisjeq  6149  nc0le1  6217  leconnnc  6219  muc0or  6253  nchoicelem9  6298  nchoicelem16  6305  nchoicelem17  6306  nchoice  6309