Theorem orbi12d 475

Description: Deduction joining two equivalences to form equivalence of disjunctions.

Hypotheses

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

Assertion

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

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		bi2d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	orbi1d 467	. 2 |- (ph -> ((ps \/ th) <-> (ch \/ th)))
3		bi2d.2	. . 3 |- (ph -> (th <-> ta ))
4	3	orbi2d 466	. 2 |- (ph -> ((ch \/ th) <-> (ch \/ ta )))
5	2, 4	bitrd 406	1 |- (ph -> ((ps \/ th) <-> (ch \/ ta )))

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

This theorem is referenced by:  bi3ord 635  eueq3 1430  sbcor 1462  elun 1601  elprg 1822  so 2152  ordtri3or 2230  ordsucun 2333  fununi 2705  funcnvuni 2706  tz7.44-2 2967  rdglem2 2976  oacan 3150  oaword 3151  ltsopq 3869  prlem934b 3932  addcanpr 3946  ltsosr 3997  ltsor 4055  letrit 4347  lemul2 4396  lerec 4411  sq11 4416  nnleltp1t 4448  elznn0 4576  nn0subt 4587  zaddclt 4590  nneo 4719  infxpidmlem2 4934  infxpidmlem7 4939  h1datomt 5484  atss 5744  atom1d 5750

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