Theorem orbi12d 793

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  822  dcbid  838  3orbi123d  1311  dfbi3dc  1397  eueq3dc  2912  sbcor  3008  sbcorg  3009  unjust  3133  elun  3277  ifbi  3555  elprg  3613  eltpg  3638  rabrsndc  3661  preq12bg  3774  exmid01  4199  exmidsssnc  4204  swopolem  4306  soeq1  4316  sowlin  4321  ordtri2orexmid  4523  regexmidlemm  4532  regexmidlem1  4533  reg2exmidlema  4534  ordsoexmid  4562  ordtri2or2exmid  4571  ontri2orexmidim  4572  nn0suc  4604  nndceq0  4618  0elnn  4619  soinxp  4697  fununi  5285  funcnvuni  5286  fun11iun  5483  unpreima  5642  isosolem  5825  xporderlem  6232  poxp  6233  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  inffiexmid  6906  fidcenumlemrk  6953  isomni  7134  enomnilem  7136  finomni  7138  exmidomni  7140  fodjuomnilemres  7146  onntri45  7240  tapeq1  7251  netap  7253  2omotaplemap  7256  indpi  7341  ltexprlemloc  7606  addextpr  7620  ltsosr  7763  aptisr  7778  mulextsr1lem  7779  mulextsr1  7780  axpre-ltwlin  7882  axpre-apti  7884  axpre-mulext  7887  axltwlin  8025  axapti  8028  axsuploc  8030  reapval  8533  reapti  8536  reapmul1lem  8551  reapmul1  8552  reapadd1  8553  reapneg  8554  reapcotr  8555  remulext1  8556  apreim  8560  apsym  8563  apcotr  8564  apadd1  8565  addext  8567  apneg  8568  nn1m1nn  8937  nn1gt1  8953  elznn0  9268  elz2  9324  nn0n0n1ge2b  9332  nneoor  9355  uztric  9549  ltxr  9775  fzsplit2  10050  uzsplit  10092  fzospliti  10176  fzouzsplit  10179  exbtwnzlemstep  10248  exbtwnzlemex  10250  qavgle  10259  frec2uzled  10429  sq11ap  10688  sqrt11ap  11047  abs00ap  11071  maxclpr  11231  minmax  11238  minclpr  11245  xrmaxiflemcom  11257  xrminmax  11273  xrminltinf  11280  sumeq1  11363  sumeq2  11367  fz1f1o  11383  summodc  11391  fsum3  11395  prodeq1f  11560  prodeq2w  11564  prodeq2  11565  prodmodc  11586  fprodseq  11591  fprodcl2lem  11613  zeo3  11873  odd2np1lem  11877  dvdsprime  12122  coprm  12144  ennnfonelemrnh  12417  islring  13333  reopnap  14041  reapef  14202  logrpap0b  14300  lgslem1  14404  decidi  14550  bj-nn0suc0  14705  bj-inf2vnlem2  14726  bj-nn0sucALT  14733  isomninnlem  14781  trilpolemlt1  14792  trirec0  14795