Theorem orbi12d 783

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

Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.39  812  dcbid  824  3orbi123d  1290  dfbi3dc  1376  eueq3dc  2862  sbcor  2957  sbcorg  2958  unjust  3079  elun  3222  ifbi  3497  elprg  3552  eltpg  3576  rabrsndc  3599  preq12bg  3708  exmid01  4129  exmidsssnc  4134  swopolem  4235  soeq1  4245  sowlin  4250  ordtri2orexmid  4446  regexmidlemm  4455  regexmidlem1  4456  reg2exmidlema  4457  ordsoexmid  4485  ordtri2or2exmid  4494  nn0suc  4526  nndceq0  4539  0elnn  4540  soinxp  4617  fununi  5199  funcnvuni  5200  fun11iun  5396  unpreima  5553  isosolem  5733  xporderlem  6136  poxp  6137  frec0g  6302  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  inffiexmid  6808  fidcenumlemrk  6850  isomni  7016  enomnilem  7018  finomni  7020  exmidomni  7022  fodjuomnilemres  7028  indpi  7174  ltexprlemloc  7439  addextpr  7453  ltsosr  7596  aptisr  7611  mulextsr1lem  7612  mulextsr1  7613  axpre-ltwlin  7715  axpre-apti  7717  axpre-mulext  7720  axltwlin  7856  axapti  7859  axsuploc  7861  reapval  8362  reapti  8365  reapmul1lem  8380  reapmul1  8381  reapadd1  8382  reapneg  8383  reapcotr  8384  remulext1  8385  apreim  8389  apsym  8392  apcotr  8393  apadd1  8394  addext  8396  apneg  8397  nn1m1nn  8762  nn1gt1  8778  elznn0  9093  elz2  9146  nn0n0n1ge2b  9154  nneoor  9177  uztric  9371  ltxr  9592  fzsplit2  9861  uzsplit  9903  fzospliti  9984  fzouzsplit  9987  exbtwnzlemstep  10056  exbtwnzlemex  10058  qavgle  10067  frec2uzled  10233  sq11ap  10489  sqrt11ap  10842  abs00ap  10866  maxclpr  11026  minmax  11033  minclpr  11040  xrmaxiflemcom  11050  xrminmax  11066  xrminltinf  11073  sumeq1  11156  sumeq2  11160  fz1f1o  11176  summodc  11184  fsum3  11188  prodeq1f  11353  prodeq2w  11357  prodeq2  11358  prodmodc  11379  fprodseq  11384  zeo3  11601  odd2np1lem  11605  dvdsprime  11839  coprm  11858  ennnfonelemrnh  11965  reopnap  12746  reapef  12907  logrpap0b  13005  decidi  13173  bj-nn0suc0  13319  bj-inf2vnlem2  13340  bj-nn0sucALT  13347  isomninnlem  13400  trilpolemlt1  13409  trirec0  13412