Theorem orbi12d 794

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

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  823  dcbid  839  3orbi123d  1322  dfbi3dc  1408  eueq3dc  2926  sbcor  3022  sbcorg  3023  unjust  3147  elun  3291  ifbi  3569  elprg  3627  eltpg  3652  rabrsndc  3675  preq12bg  3788  exmid01  4213  exmidsssnc  4218  swopolem  4320  soeq1  4330  sowlin  4335  ordtri2orexmid  4537  regexmidlemm  4546  regexmidlem1  4547  reg2exmidlema  4548  ordsoexmid  4576  ordtri2or2exmid  4585  ontri2orexmidim  4586  nn0suc  4618  nndceq0  4632  0elnn  4633  soinxp  4711  fununi  5300  funcnvuni  5301  fun11iun  5498  unpreima  5658  isosolem  5842  xporderlem  6251  poxp  6252  frec0g  6417  freccllem  6422  frecfcllem  6424  frecsuclem  6426  frecsuc  6427  inffiexmid  6929  fidcenumlemrk  6978  isomni  7159  enomnilem  7161  finomni  7163  exmidomni  7165  fodjuomnilemres  7171  onntri45  7265  tapeq1  7276  netap  7278  2omotaplemap  7281  indpi  7366  ltexprlemloc  7631  addextpr  7645  ltsosr  7788  aptisr  7803  mulextsr1lem  7804  mulextsr1  7805  axpre-ltwlin  7907  axpre-apti  7909  axpre-mulext  7912  axltwlin  8050  axapti  8053  axsuploc  8055  reapval  8558  reapti  8561  reapmul1lem  8576  reapmul1  8577  reapadd1  8578  reapneg  8579  reapcotr  8580  remulext1  8581  apreim  8585  apsym  8588  apcotr  8589  apadd1  8590  addext  8592  apneg  8593  nn1m1nn  8962  nn1gt1  8978  elznn0  9293  elz2  9349  nn0n0n1ge2b  9357  nneoor  9380  uztric  9574  ltxr  9800  fzsplit2  10075  uzsplit  10117  fzospliti  10201  fzouzsplit  10204  exbtwnzlemstep  10273  exbtwnzlemex  10275  qavgle  10284  frec2uzled  10455  sq11ap  10714  sqrt11ap  11074  abs00ap  11098  maxclpr  11258  minmax  11265  minclpr  11272  xrmaxiflemcom  11284  xrminmax  11300  xrminltinf  11307  sumeq1  11390  sumeq2  11394  fz1f1o  11410  summodc  11418  fsum3  11422  prodeq1f  11587  prodeq2w  11591  prodeq2  11592  prodmodc  11613  fprodseq  11618  fprodcl2lem  11640  zeo3  11900  odd2np1lem  11904  dvdsprime  12149  coprm  12171  ennnfonelemrnh  12462  islring  13532  reopnap  14475  reapef  14636  logrpap0b  14734  wilthlem1  14835  lgslem1  14839  decidi  14985  bj-nn0suc0  15140  bj-inf2vnlem2  15161  bj-nn0sucALT  15168  isomninnlem  15217  trilpolemlt1  15228  trirec0  15231