Theorem orbi12d 795

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  824  dcbid  840  3orbi123d  1324  dfbi3dc  1417  eueq3dc  2951  sbcor  3047  sbcorg  3048  unjust  3173  elun  3318  ifbi  3595  elprg  3657  eltpg  3682  rabrsndc  3705  preq12bg  3819  exmid01  4249  exmidsssnc  4254  swopolem  4359  soeq1  4369  sowlin  4374  ordtri2orexmid  4578  regexmidlemm  4587  regexmidlem1  4588  reg2exmidlema  4589  ordsoexmid  4617  ordtri2or2exmid  4626  ontri2orexmidim  4627  nn0suc  4659  nndceq0  4673  0elnn  4674  soinxp  4752  fununi  5350  funcnvuni  5351  fun11iun  5554  unpreima  5717  isosolem  5905  xporderlem  6329  poxp  6330  frec0g  6495  freccllem  6500  frecfcllem  6502  frecsuclem  6504  frecsuc  6505  inffiexmid  7017  fidcenumlemrk  7070  isomni  7252  enomnilem  7254  finomni  7256  exmidomni  7258  fodjuomnilemres  7264  onntri45  7368  tapeq1  7379  netap  7381  2omotaplemap  7384  indpi  7470  ltexprlemloc  7735  addextpr  7749  ltsosr  7892  aptisr  7907  mulextsr1lem  7908  mulextsr1  7909  axpre-ltwlin  8011  axpre-apti  8013  axpre-mulext  8016  axltwlin  8155  axapti  8158  axsuploc  8160  reapval  8664  reapti  8667  reapmul1lem  8682  reapmul1  8683  reapadd1  8684  reapneg  8685  reapcotr  8686  remulext1  8687  apreim  8691  apsym  8694  apcotr  8695  apadd1  8696  addext  8698  apneg  8699  nn1m1nn  9069  nn1gt1  9085  elznn0  9402  elz2  9459  nn0n0n1ge2b  9467  nneoor  9490  uztric  9685  ltxr  9912  fzsplit2  10187  uzsplit  10229  nelfzo  10289  fzospliti  10315  fzouzsplit  10318  exbtwnzlemstep  10407  exbtwnzlemex  10409  qavgle  10418  frec2uzled  10591  sq11ap  10869  swrdnd  11130  sqrt11ap  11419  abs00ap  11443  maxclpr  11603  minmax  11611  minclpr  11618  xrmaxiflemcom  11630  xrminmax  11646  xrminltinf  11653  sumeq1  11736  sumeq2  11740  fz1f1o  11756  summodc  11764  fsum3  11768  prodeq1f  11933  prodeq2w  11937  prodeq2  11938  prodmodc  11959  fprodseq  11964  fprodcl2lem  11986  zeo3  12249  odd2np1lem  12253  dvdsprime  12514  coprm  12536  ennnfonelemrnh  12857  igsumvalx  13291  gsumfzval  13293  gsumpropd  13294  gsumpropd2  13295  gsumress  13297  gsum0g  13298  islring  14024  isdomn  14101  opprdomnbg  14106  znidom  14489  reopnap  15088  dich0  15194  reapef  15320  logrpap0b  15418  wilthlem1  15522  perfectlem2  15542  lgslem1  15547  upgrm  15766  upgr1or2  15767  upgr1elem1  15783  decidi  15865  bj-nn0suc0  16020  bj-inf2vnlem2  16041  bj-nn0sucALT  16048  isomninnlem  16104  trilpolemlt1  16115  trirec0  16118