Theorem orbi12d 798

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  827  dcbid  843  ifpbi123d  998  3orbi123d  1345  dfbi3dc  1439  eueq3dc  2977  sbcor  3073  sbcorg  3074  unjust  3200  elun  3345  elif  3614  ifbi  3623  elprg  3686  eltpg  3711  rabrsndc  3734  preq12bg  3850  exmid01  4281  exmidsssnc  4286  swopolem  4395  soeq1  4405  sowlin  4410  ordtri2orexmid  4614  regexmidlemm  4623  regexmidlem1  4624  reg2exmidlema  4625  ordsoexmid  4653  ordtri2or2exmid  4662  ontri2orexmidim  4663  nn0suc  4695  nndceq0  4709  0elnn  4710  soinxp  4788  fununi  5388  funcnvuni  5389  fun11iun  5592  unpreima  5759  isosolem  5947  xporderlem  6375  poxp  6376  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  inffiexmid  7064  fidcenumlemrk  7117  isomni  7299  enomnilem  7301  finomni  7303  exmidomni  7305  fodjuomnilemres  7311  onntri45  7422  tapeq1  7434  netap  7436  2omotaplemap  7439  indpi  7525  ltexprlemloc  7790  addextpr  7804  ltsosr  7947  aptisr  7962  mulextsr1lem  7963  mulextsr1  7964  axpre-ltwlin  8066  axpre-apti  8068  axpre-mulext  8071  axltwlin  8210  axapti  8213  axsuploc  8215  reapval  8719  reapti  8722  reapmul1lem  8737  reapmul1  8738  reapadd1  8739  reapneg  8740  reapcotr  8741  remulext1  8742  apreim  8746  apsym  8749  apcotr  8750  apadd1  8751  addext  8753  apneg  8754  nn1m1nn  9124  nn1gt1  9140  elznn0  9457  elz2  9514  nn0n0n1ge2b  9522  nneoor  9545  uztric  9740  ltxr  9967  fzsplit2  10242  uzsplit  10284  nelfzo  10344  fzospliti  10370  fzouzsplit  10373  exbtwnzlemstep  10462  exbtwnzlemex  10464  qavgle  10473  frec2uzled  10646  sq11ap  10924  swrdnd  11186  sqrt11ap  11544  abs00ap  11568  maxclpr  11728  minmax  11736  minclpr  11743  xrmaxiflemcom  11755  xrminmax  11771  xrminltinf  11778  sumeq1  11861  sumeq2  11865  fz1f1o  11881  summodc  11889  fsum3  11893  prodeq1f  12058  prodeq2w  12062  prodeq2  12063  prodmodc  12084  fprodseq  12089  fprodcl2lem  12111  zeo3  12374  odd2np1lem  12378  dvdsprime  12639  coprm  12661  ennnfonelemrnh  12982  igsumvalx  13417  gsumfzval  13419  gsumpropd  13420  gsumpropd2  13421  gsumress  13423  gsum0g  13424  islring  14150  isdomn  14227  opprdomnbg  14232  znidom  14615  reopnap  15214  dich0  15320  reapef  15446  logrpap0b  15544  wilthlem1  15648  perfectlem2  15668  lgslem1  15673  upgrm  15894  upgr1or2  15895  upgr1elem1  15914  edgupgren  15933  usgruspgrben  15978  decidi  16117  bj-nn0suc0  16271  bj-inf2vnlem2  16292  bj-nn0sucALT  16299  isomninnlem  16357  trilpolemlt1  16368  trirec0  16371