Theorem orbi12d 801

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  830  dcbid  846  ifpbi123d  1001  3orbi123d  1348  dfbi3dc  1442  eueq3dc  2991  sbcor  3087  sbcorg  3088  unjust  3214  elun  3360  elif  3634  ifbi  3643  elprg  3709  eltpg  3734  rabsnifsb  3757  rabrsndc  3759  preq12bg  3877  exmid01  4311  exmidsssnc  4316  swopolem  4426  soeq1  4436  sowlin  4441  ordtri2orexmid  4645  regexmidlemm  4654  regexmidlem1  4655  reg2exmidlema  4656  ordsoexmid  4684  ordtri2or2exmid  4693  ontri2orexmidim  4694  nn0suc  4726  nndceq0  4740  0elnn  4741  soinxp  4820  fununi  5424  funcnvuni  5425  fun11iun  5635  unpreima  5802  isosolem  5997  xporderlem  6427  poxp  6428  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  inffiexmid  7166  fidcenumlemrk  7224  isomni  7427  enomnilem  7429  finomni  7431  exmidomni  7433  fodjuomnilemres  7439  onntri45  7551  papcotr  7562  tapeq1  7566  netap  7568  2omotaplemap  7571  indpi  7657  ltexprlemloc  7922  addextpr  7936  ltsosr  8079  aptisr  8094  mulextsr1lem  8095  mulextsr1  8096  axpre-ltwlin  8198  axpre-apti  8200  axpre-mulext  8203  axltwlin  8341  axapti  8344  axsuploc  8346  reapval  8850  reapti  8853  reapmul1lem  8868  reapmul1  8869  reapadd1  8870  reapneg  8871  reapcotr  8872  remulext1  8873  apreim  8877  apsym  8880  apcotr  8881  apadd1  8882  addext  8884  apneg  8885  nn1m1nn  9255  nn1gt1  9271  elznn0  9592  elz2  9649  nn0n0n1ge2b  9657  nneoor  9680  uztric  9876  ltxr  10108  fzsplit2  10384  uzsplit  10426  nelfzo  10486  fzospliti  10512  fzouzsplit  10515  exbtwnzlemstep  10607  exbtwnzlemex  10609  qavgle  10618  frec2uzled  10791  sq11ap  11069  swrdnd  11351  sqrt11ap  11723  abs00ap  11747  maxclpr  11907  minmax  11915  minclpr  11922  xrmaxiflemcom  11934  xrminmax  11950  xrminltinf  11957  sumeq1  12040  sumeq2  12044  fz1f1o  12060  summodc  12069  fsum3  12073  prodeq1f  12238  prodeq2w  12242  prodeq2  12243  prodmodc  12264  fprodseq  12269  fprodcl2lem  12291  zeo3  12554  odd2np1lem  12558  dvdsprime  12819  coprm  12841  ennnfonelemrnh  13167  igsumvalx  13602  gsumfzval  13604  gsumpropd  13605  gsumpropd2  13606  gsumress  13608  gsum0g  13609  islring  14337  isdomn  14415  opprdomnbg  14420  znidom  14805  reopnap  15411  dich0  15517  reapef  15643  logrpap0b  15741  wilthlem1  15848  perfectlem2  15868  lgslem1  15873  upgrm  16095  upgr1or2  16096  upgr1elem1  16115  edgupgren  16136  usgruspgrben  16181  subupgr  16268  konigsberglem1  16483  decidi  16567  bj-nn0suc0  16720  bj-inf2vnlem2  16741  bj-nn0sucALT  16748  isomninnlem  16814  trilpolemlt1  16825  trirec0  16828