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  5299  funcnvuni  5300  fun11iun  5497  unpreima  5657  isosolem  5841  xporderlem  6250  poxp  6251  frec0g  6416  freccllem  6421  frecfcllem  6423  frecsuclem  6425  frecsuc  6426  inffiexmid  6924  fidcenumlemrk  6971  isomni  7152  enomnilem  7154  finomni  7156  exmidomni  7158  fodjuomnilemres  7164  onntri45  7258  tapeq1  7269  netap  7271  2omotaplemap  7274  indpi  7359  ltexprlemloc  7624  addextpr  7638  ltsosr  7781  aptisr  7796  mulextsr1lem  7797  mulextsr1  7798  axpre-ltwlin  7900  axpre-apti  7902  axpre-mulext  7905  axltwlin  8043  axapti  8046  axsuploc  8048  reapval  8551  reapti  8554  reapmul1lem  8569  reapmul1  8570  reapadd1  8571  reapneg  8572  reapcotr  8573  remulext1  8574  apreim  8578  apsym  8581  apcotr  8582  apadd1  8583  addext  8585  apneg  8586  nn1m1nn  8955  nn1gt1  8971  elznn0  9286  elz2  9342  nn0n0n1ge2b  9350  nneoor  9373  uztric  9567  ltxr  9793  fzsplit2  10068  uzsplit  10110  fzospliti  10194  fzouzsplit  10197  exbtwnzlemstep  10266  exbtwnzlemex  10268  qavgle  10277  frec2uzled  10447  sq11ap  10706  sqrt11ap  11065  abs00ap  11089  maxclpr  11249  minmax  11256  minclpr  11263  xrmaxiflemcom  11275  xrminmax  11291  xrminltinf  11298  sumeq1  11381  sumeq2  11385  fz1f1o  11401  summodc  11409  fsum3  11413  prodeq1f  11578  prodeq2w  11582  prodeq2  11583  prodmodc  11604  fprodseq  11609  fprodcl2lem  11631  zeo3  11891  odd2np1lem  11895  dvdsprime  12140  coprm  12162  ennnfonelemrnh  12435  islring  13500  reopnap  14435  reapef  14596  logrpap0b  14694  lgslem1  14798  decidi  14944  bj-nn0suc0  15099  bj-inf2vnlem2  15120  bj-nn0sucALT  15127  isomninnlem  15176  trilpolemlt1  15187  trirec0  15190