Theorem orbi12d 788

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.39  817  dcbid  833  3orbi123d  1306  dfbi3dc  1392  eueq3dc  2904  sbcor  2999  sbcorg  3000  unjust  3124  elun  3268  ifbi  3546  elprg  3603  eltpg  3628  rabrsndc  3651  preq12bg  3760  exmid01  4184  exmidsssnc  4189  swopolem  4290  soeq1  4300  sowlin  4305  ordtri2orexmid  4507  regexmidlemm  4516  regexmidlem1  4517  reg2exmidlema  4518  ordsoexmid  4546  ordtri2or2exmid  4555  ontri2orexmidim  4556  nn0suc  4588  nndceq0  4602  0elnn  4603  soinxp  4681  fununi  5266  funcnvuni  5267  fun11iun  5463  unpreima  5621  isosolem  5803  xporderlem  6210  poxp  6211  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  inffiexmid  6884  fidcenumlemrk  6931  isomni  7112  enomnilem  7114  finomni  7116  exmidomni  7118  fodjuomnilemres  7124  onntri45  7218  indpi  7304  ltexprlemloc  7569  addextpr  7583  ltsosr  7726  aptisr  7741  mulextsr1lem  7742  mulextsr1  7743  axpre-ltwlin  7845  axpre-apti  7847  axpre-mulext  7850  axltwlin  7987  axapti  7990  axsuploc  7992  reapval  8495  reapti  8498  reapmul1lem  8513  reapmul1  8514  reapadd1  8515  reapneg  8516  reapcotr  8517  remulext1  8518  apreim  8522  apsym  8525  apcotr  8526  apadd1  8527  addext  8529  apneg  8530  nn1m1nn  8896  nn1gt1  8912  elznn0  9227  elz2  9283  nn0n0n1ge2b  9291  nneoor  9314  uztric  9508  ltxr  9732  fzsplit2  10006  uzsplit  10048  fzospliti  10132  fzouzsplit  10135  exbtwnzlemstep  10204  exbtwnzlemex  10206  qavgle  10215  frec2uzled  10385  sq11ap  10643  sqrt11ap  11002  abs00ap  11026  maxclpr  11186  minmax  11193  minclpr  11200  xrmaxiflemcom  11212  xrminmax  11228  xrminltinf  11235  sumeq1  11318  sumeq2  11322  fz1f1o  11338  summodc  11346  fsum3  11350  prodeq1f  11515  prodeq2w  11519  prodeq2  11520  prodmodc  11541  fprodseq  11546  fprodcl2lem  11568  zeo3  11827  odd2np1lem  11831  dvdsprime  12076  coprm  12098  ennnfonelemrnh  12371  reopnap  13332  reapef  13493  logrpap0b  13591  lgslem1  13695  decidi  13830  bj-nn0suc0  13985  bj-inf2vnlem2  14006  bj-nn0sucALT  14013  isomninnlem  14062  trilpolemlt1  14073  trirec0  14076