Theorem orbi12d 740

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 738	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		orbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 737	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 186	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 103   ∨ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm4.39  769  dcbid  782  3orbi123d  1243  dfbi3dc  1329  eueq3dc  2767  sbcor  2859  sbcorg  2860  unjust  2977  elun  3114  ifbi  3377  elprg  3426  eltpg  3446  rabrsndc  3468  preq12bg  3573  swopolem  4068  soeq1  4078  sowlin  4083  ordtri2orexmid  4274  regexmidlemm  4283  regexmidlem1  4284  reg2exmidlema  4285  ordsoexmid  4313  ordtri2or2exmid  4322  nn0suc  4353  nndceq0  4365  0elnn  4366  soinxp  4436  fununi  4998  funcnvuni  4999  fun11iun  5178  unpreima  5324  isosolem  5494  xporderlem  5883  poxp  5884  frec0g  6046  freccllem  6051  frecfcllem  6053  frecsuclem  6055  frecsuc  6056  indpi  6594  ltexprlemloc  6859  addextpr  6873  ltsosr  7003  aptisr  7017  mulextsr1lem  7018  mulextsr1  7019  axpre-ltwlin  7111  axpre-apti  7113  axpre-mulext  7116  axltwlin  7247  axapti  7250  reapval  7743  reapti  7746  reapmul1lem  7761  reapmul1  7762  reapadd1  7763  reapneg  7764  reapcotr  7765  remulext1  7766  apreim  7770  apsym  7773  apcotr  7774  apadd1  7775  addext  7777  apneg  7778  nn1m1nn  8124  nn1gt1  8139  elznn0  8447  elz2  8500  nn0n0n1ge2b  8508  nneoor  8530  uztric  8721  ltxr  8927  fzsplit2  9145  uzsplit  9185  fzospliti  9262  fzouzsplit  9265  exbtwnzlemstep  9334  exbtwnzlemex  9336  qavgle  9345  frec2uzled  9511  sq11ap  9736  sqrt11ap  10062  abs00ap  10086  maxclpr  10246  minmax  10250  sumeq1  10330  sumeq2d  10334  sumeq2  10335  fz1f1o  10336  zeo3  10412  odd2np1lem  10416  dvdsprime  10648  coprm  10667  decidi  10756  bj-dcbi  10877  bj-nn0suc0  10903  bj-inf2vnlem2  10924  bj-nn0sucALT  10931