Theorem orbi12d 625

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

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

This theorem is referenced by:  pm4.39 628  3orbi123d 889  eueq3 1910  sbcorg 1962  elun 2163  elprg 2413  so 2855  ordtri3or 2969  ordsucun 3072  fununi 3549  funcnvuni 3550  tz7.44-2 3914  rdglem2 3923  oacan 4166  oaword 4167  omword 4185  oeword 4201  ltsopq 5047  prlem934b 5110  addcanpr 5124  ltsosr 5175  ltsor 5233  ltxrt 5467  xrrebndt 5541  lemul1t 5788  lerec 5828  msq11 5831  nnleltp1t 5901  avglet 5991  elznn0 6096  nn0subt 6108  zaddclt 6112  nneo 6144  sqeqort 6580  bcval4t 6899  infxpidmlem2 7496  infxpidmlem7 7501  fctop 7592  cctop 7594  h1datomt 9422  atss 10181  atom1d 10188  atordt 10223  irredt 10230  erdisj2 10343

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