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  1293  dfbi3dc  1379  eueq3dc  2886  sbcor  2981  sbcorg  2982  unjust  3105  elun  3248  ifbi  3525  elprg  3580  eltpg  3604  rabrsndc  3627  preq12bg  3736  exmid01  4159  exmidsssnc  4164  swopolem  4265  soeq1  4275  sowlin  4280  ordtri2orexmid  4482  regexmidlemm  4491  regexmidlem1  4492  reg2exmidlema  4493  ordsoexmid  4521  ordtri2or2exmid  4530  ontri2orexmidim  4531  nn0suc  4563  nndceq0  4577  0elnn  4578  soinxp  4656  fununi  5238  funcnvuni  5239  fun11iun  5435  unpreima  5592  isosolem  5774  xporderlem  6178  poxp  6179  frec0g  6344  freccllem  6349  frecfcllem  6351  frecsuclem  6353  frecsuc  6354  inffiexmid  6851  fidcenumlemrk  6898  isomni  7079  enomnilem  7081  finomni  7083  exmidomni  7085  fodjuomnilemres  7091  onntri45  7176  indpi  7262  ltexprlemloc  7527  addextpr  7541  ltsosr  7684  aptisr  7699  mulextsr1lem  7700  mulextsr1  7701  axpre-ltwlin  7803  axpre-apti  7805  axpre-mulext  7808  axltwlin  7945  axapti  7948  axsuploc  7950  reapval  8451  reapti  8454  reapmul1lem  8469  reapmul1  8470  reapadd1  8471  reapneg  8472  reapcotr  8473  remulext1  8474  apreim  8478  apsym  8481  apcotr  8482  apadd1  8483  addext  8485  apneg  8486  nn1m1nn  8851  nn1gt1  8867  elznn0  9182  elz2  9235  nn0n0n1ge2b  9243  nneoor  9266  uztric  9460  ltxr  9682  fzsplit2  9952  uzsplit  9994  fzospliti  10075  fzouzsplit  10078  exbtwnzlemstep  10147  exbtwnzlemex  10149  qavgle  10158  frec2uzled  10328  sq11ap  10585  sqrt11ap  10938  abs00ap  10962  maxclpr  11122  minmax  11129  minclpr  11136  xrmaxiflemcom  11146  xrminmax  11162  xrminltinf  11169  sumeq1  11252  sumeq2  11256  fz1f1o  11272  summodc  11280  fsum3  11284  prodeq1f  11449  prodeq2w  11453  prodeq2  11454  prodmodc  11475  fprodseq  11480  fprodcl2lem  11502  zeo3  11759  odd2np1lem  11763  dvdsprime  11999  coprm  12019  ennnfonelemrnh  12156  reopnap  12949  reapef  13110  logrpap0b  13208  decidi  13380  bj-nn0suc0  13536  bj-inf2vnlem2  13557  bj-nn0sucALT  13564  isomninnlem  13612  trilpolemlt1  13623  trirec0  13626