Theorem orbi12d 627

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

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 615	. 2 |- (ph -> ((ps \/ th) <-> (ch \/ th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	orbi2d 614	. 2 |- (ph -> ((ch \/ th) <-> (ch \/ ta)))
5	2, 4	bitrd 528	1 |- (ph -> ((ps \/ th) <-> (ch \/ ta)))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222

This theorem is referenced by:  pm4.39 630  3orbi123d 892  eueq3 1919  sbcorg 1972  elun 2173  elprg 2423  so 2864  ordtri3or 2979  ordsucun 3082  fununi 3563  funcnvuni 3564  tz7.44-2 3929  rdglem2 3938  oacan 4182  oaword 4183  omword 4201  oeword 4217  ltsopq 5075  prlem934b 5138  addcanpr 5152  ltsosr 5203  ltsor 5261  ltxrt 5495  xrrebndt 5568  lemul1t 5832  lerec 5880  msq11 5883  nnleltp1t 5954  avglet 6044  elznn0 6149  nn0subt 6161  zaddclt 6165  nneo 6197  ioojoint 6416  sqeqort 6649  bcval4t 6961  infxpidmlem2 7553  infxpidmlem7 7558  fctopOLD 7650  cctop 7652  h1datomt 9505  atss 10273  atom1d 10280  atordt 10315  irredt 10322  erdisj2 10442

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain