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  2938  sbcor  3034  sbcorg  3035  unjust  3160  elun  3304  ifbi  3581  elprg  3642  eltpg  3667  rabrsndc  3690  preq12bg  3803  exmid01  4231  exmidsssnc  4236  swopolem  4340  soeq1  4350  sowlin  4355  ordtri2orexmid  4559  regexmidlemm  4568  regexmidlem1  4569  reg2exmidlema  4570  ordsoexmid  4598  ordtri2or2exmid  4607  ontri2orexmidim  4608  nn0suc  4640  nndceq0  4654  0elnn  4655  soinxp  4733  fununi  5326  funcnvuni  5327  fun11iun  5525  unpreima  5687  isosolem  5871  xporderlem  6289  poxp  6290  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  inffiexmid  6967  fidcenumlemrk  7020  isomni  7202  enomnilem  7204  finomni  7206  exmidomni  7208  fodjuomnilemres  7214  onntri45  7308  tapeq1  7319  netap  7321  2omotaplemap  7324  indpi  7409  ltexprlemloc  7674  addextpr  7688  ltsosr  7831  aptisr  7846  mulextsr1lem  7847  mulextsr1  7848  axpre-ltwlin  7950  axpre-apti  7952  axpre-mulext  7955  axltwlin  8094  axapti  8097  axsuploc  8099  reapval  8603  reapti  8606  reapmul1lem  8621  reapmul1  8622  reapadd1  8623  reapneg  8624  reapcotr  8625  remulext1  8626  apreim  8630  apsym  8633  apcotr  8634  apadd1  8635  addext  8637  apneg  8638  nn1m1nn  9008  nn1gt1  9024  elznn0  9341  elz2  9397  nn0n0n1ge2b  9405  nneoor  9428  uztric  9623  ltxr  9850  fzsplit2  10125  uzsplit  10167  nelfzo  10227  fzospliti  10252  fzouzsplit  10255  exbtwnzlemstep  10337  exbtwnzlemex  10339  qavgle  10348  frec2uzled  10521  sq11ap  10799  sqrt11ap  11203  abs00ap  11227  maxclpr  11387  minmax  11395  minclpr  11402  xrmaxiflemcom  11414  xrminmax  11430  xrminltinf  11437  sumeq1  11520  sumeq2  11524  fz1f1o  11540  summodc  11548  fsum3  11552  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  prodmodc  11743  fprodseq  11748  fprodcl2lem  11770  zeo3  12033  odd2np1lem  12037  dvdsprime  12290  coprm  12312  ennnfonelemrnh  12633  igsumvalx  13032  gsumfzval  13034  gsumpropd  13035  gsumpropd2  13036  gsumress  13038  gsum0g  13039  islring  13748  isdomn  13825  opprdomnbg  13830  znidom  14213  reopnap  14782  dich0  14888  reapef  15014  logrpap0b  15112  wilthlem1  15216  perfectlem2  15236  lgslem1  15241  decidi  15441  bj-nn0suc0  15596  bj-inf2vnlem2  15617  bj-nn0sucALT  15624  isomninnlem  15674  trilpolemlt1  15685  trirec0  15688