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  2935  sbcor  3031  sbcorg  3032  unjust  3157  elun  3301  ifbi  3578  elprg  3639  eltpg  3664  rabrsndc  3687  preq12bg  3800  exmid01  4228  exmidsssnc  4233  swopolem  4337  soeq1  4347  sowlin  4352  ordtri2orexmid  4556  regexmidlemm  4565  regexmidlem1  4566  reg2exmidlema  4567  ordsoexmid  4595  ordtri2or2exmid  4604  ontri2orexmidim  4605  nn0suc  4637  nndceq0  4651  0elnn  4652  soinxp  4730  fununi  5323  funcnvuni  5324  fun11iun  5522  unpreima  5684  isosolem  5868  xporderlem  6286  poxp  6287  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  inffiexmid  6964  fidcenumlemrk  7015  isomni  7197  enomnilem  7199  finomni  7201  exmidomni  7203  fodjuomnilemres  7209  onntri45  7303  tapeq1  7314  netap  7316  2omotaplemap  7319  indpi  7404  ltexprlemloc  7669  addextpr  7683  ltsosr  7826  aptisr  7841  mulextsr1lem  7842  mulextsr1  7843  axpre-ltwlin  7945  axpre-apti  7947  axpre-mulext  7950  axltwlin  8089  axapti  8092  axsuploc  8094  reapval  8597  reapti  8600  reapmul1lem  8615  reapmul1  8616  reapadd1  8617  reapneg  8618  reapcotr  8619  remulext1  8620  apreim  8624  apsym  8627  apcotr  8628  apadd1  8629  addext  8631  apneg  8632  nn1m1nn  9002  nn1gt1  9018  elznn0  9335  elz2  9391  nn0n0n1ge2b  9399  nneoor  9422  uztric  9617  ltxr  9844  fzsplit2  10119  uzsplit  10161  nelfzo  10221  fzospliti  10246  fzouzsplit  10249  exbtwnzlemstep  10319  exbtwnzlemex  10321  qavgle  10330  frec2uzled  10503  sq11ap  10781  sqrt11ap  11185  abs00ap  11209  maxclpr  11369  minmax  11376  minclpr  11383  xrmaxiflemcom  11395  xrminmax  11411  xrminltinf  11418  sumeq1  11501  sumeq2  11505  fz1f1o  11521  summodc  11529  fsum3  11533  prodeq1f  11698  prodeq2w  11702  prodeq2  11703  prodmodc  11724  fprodseq  11729  fprodcl2lem  11751  zeo3  12012  odd2np1lem  12016  dvdsprime  12263  coprm  12285  ennnfonelemrnh  12576  igsumvalx  12975  gsumfzval  12977  gsumpropd  12978  gsumpropd2  12979  gsumress  12981  gsum0g  12982  islring  13691  isdomn  13768  opprdomnbg  13773  znidom  14156  reopnap  14725  dich0  14831  reapef  14954  logrpap0b  15052  wilthlem1  15153  lgslem1  15157  decidi  15357  bj-nn0suc0  15512  bj-inf2vnlem2  15533  bj-nn0sucALT  15540  isomninnlem  15590  trilpolemlt1  15601  trirec0  15604