Theorem orbi12d 745

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

Hypotheses

Ref	Expression
orbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
orbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
orbi12d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		orbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi1d 743	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		orbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 742	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 667

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.39  774  dcbid  789  3orbi123d  1254  dfbi3dc  1340  eueq3dc  2803  sbcor  2897  sbcorg  2898  unjust  3016  elun  3156  ifbi  3431  elprg  3486  eltpg  3508  rabrsndc  3530  preq12bg  3639  exmid01  4053  swopolem  4156  soeq1  4166  sowlin  4171  ordtri2orexmid  4367  regexmidlemm  4376  regexmidlem1  4377  reg2exmidlema  4378  ordsoexmid  4406  ordtri2or2exmid  4415  nn0suc  4447  nndceq0  4459  0elnn  4460  soinxp  4537  fununi  5116  funcnvuni  5117  fun11iun  5309  unpreima  5463  isosolem  5641  xporderlem  6034  poxp  6035  frec0g  6200  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecsuc  6210  inffiexmid  6702  fidcenumlemrk  6743  isomni  6879  enomnilem  6881  finomni  6883  exmidomni  6885  fodjuomnilemres  6891  indpi  6998  ltexprlemloc  7263  addextpr  7277  ltsosr  7407  aptisr  7421  mulextsr1lem  7422  mulextsr1  7423  axpre-ltwlin  7515  axpre-apti  7517  axpre-mulext  7520  axltwlin  7651  axapti  7654  reapval  8150  reapti  8153  reapmul1lem  8168  reapmul1  8169  reapadd1  8170  reapneg  8171  reapcotr  8172  remulext1  8173  apreim  8177  apsym  8180  apcotr  8181  apadd1  8182  addext  8184  apneg  8185  nn1m1nn  8538  nn1gt1  8554  elznn0  8863  elz2  8916  nn0n0n1ge2b  8924  nneoor  8947  uztric  9139  ltxr  9345  fzsplit2  9613  uzsplit  9655  fzospliti  9736  fzouzsplit  9739  exbtwnzlemstep  9808  exbtwnzlemex  9810  qavgle  9819  frec2uzled  9985  sq11ap  10251  sqrt11ap  10602  abs00ap  10626  maxclpr  10786  minmax  10792  minclpr  10799  xrmaxiflemcom  10808  xrminmax  10824  xrminltinf  10831  sumeq1  10914  sumeq2  10918  fz1f1o  10934  summodc  10942  fsum3  10946  zeo3  11311  odd2np1lem  11315  dvdsprime  11547  coprm  11566  decidi  12419  bj-dcbi  12543  bj-nn0suc0  12569  bj-inf2vnlem2  12590  bj-nn0sucALT  12597