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  1321  dfbi3dc  1407  eueq3dc  2923  sbcor  3019  sbcorg  3020  unjust  3144  elun  3288  ifbi  3566  elprg  3624  eltpg  3649  rabrsndc  3672  preq12bg  3785  exmid01  4210  exmidsssnc  4215  swopolem  4317  soeq1  4327  sowlin  4332  ordtri2orexmid  4534  regexmidlemm  4543  regexmidlem1  4544  reg2exmidlema  4545  ordsoexmid  4573  ordtri2or2exmid  4582  ontri2orexmidim  4583  nn0suc  4615  nndceq0  4629  0elnn  4630  soinxp  4708  fununi  5296  funcnvuni  5297  fun11iun  5494  unpreima  5654  isosolem  5838  xporderlem  6245  poxp  6246  frec0g  6411  freccllem  6416  frecfcllem  6418  frecsuclem  6420  frecsuc  6421  inffiexmid  6919  fidcenumlemrk  6966  isomni  7147  enomnilem  7149  finomni  7151  exmidomni  7153  fodjuomnilemres  7159  onntri45  7253  tapeq1  7264  netap  7266  2omotaplemap  7269  indpi  7354  ltexprlemloc  7619  addextpr  7633  ltsosr  7776  aptisr  7791  mulextsr1lem  7792  mulextsr1  7793  axpre-ltwlin  7895  axpre-apti  7897  axpre-mulext  7900  axltwlin  8038  axapti  8041  axsuploc  8043  reapval  8546  reapti  8549  reapmul1lem  8564  reapmul1  8565  reapadd1  8566  reapneg  8567  reapcotr  8568  remulext1  8569  apreim  8573  apsym  8576  apcotr  8577  apadd1  8578  addext  8580  apneg  8581  nn1m1nn  8950  nn1gt1  8966  elznn0  9281  elz2  9337  nn0n0n1ge2b  9345  nneoor  9368  uztric  9562  ltxr  9788  fzsplit2  10063  uzsplit  10105  fzospliti  10189  fzouzsplit  10192  exbtwnzlemstep  10261  exbtwnzlemex  10263  qavgle  10272  frec2uzled  10442  sq11ap  10701  sqrt11ap  11060  abs00ap  11084  maxclpr  11244  minmax  11251  minclpr  11258  xrmaxiflemcom  11270  xrminmax  11286  xrminltinf  11293  sumeq1  11376  sumeq2  11380  fz1f1o  11396  summodc  11404  fsum3  11408  prodeq1f  11573  prodeq2w  11577  prodeq2  11578  prodmodc  11599  fprodseq  11604  fprodcl2lem  11626  zeo3  11886  odd2np1lem  11890  dvdsprime  12135  coprm  12157  ennnfonelemrnh  12430  islring  13395  reopnap  14265  reapef  14426  logrpap0b  14524  lgslem1  14628  decidi  14774  bj-nn0suc0  14929  bj-inf2vnlem2  14950  bj-nn0sucALT  14957  isomninnlem  15006  trilpolemlt1  15017  trirec0  15020