Theorem orbi12d 798

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  827  dcbid  843  ifpbi123d  998  3orbi123d  1345  dfbi3dc  1439  eueq3dc  2977  sbcor  3073  sbcorg  3074  unjust  3200  elun  3345  elif  3614  ifbi  3623  elprg  3686  eltpg  3711  rabrsndc  3734  preq12bg  3851  exmid01  4282  exmidsssnc  4287  swopolem  4396  soeq1  4406  sowlin  4411  ordtri2orexmid  4615  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  ordsoexmid  4654  ordtri2or2exmid  4663  ontri2orexmidim  4664  nn0suc  4696  nndceq0  4710  0elnn  4711  soinxp  4789  fununi  5389  funcnvuni  5390  fun11iun  5595  unpreima  5762  isosolem  5954  xporderlem  6383  poxp  6384  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  inffiexmid  7079  fidcenumlemrk  7132  isomni  7314  enomnilem  7316  finomni  7318  exmidomni  7320  fodjuomnilemres  7326  onntri45  7437  tapeq1  7449  netap  7451  2omotaplemap  7454  indpi  7540  ltexprlemloc  7805  addextpr  7819  ltsosr  7962  aptisr  7977  mulextsr1lem  7978  mulextsr1  7979  axpre-ltwlin  8081  axpre-apti  8083  axpre-mulext  8086  axltwlin  8225  axapti  8228  axsuploc  8230  reapval  8734  reapti  8737  reapmul1lem  8752  reapmul1  8753  reapadd1  8754  reapneg  8755  reapcotr  8756  remulext1  8757  apreim  8761  apsym  8764  apcotr  8765  apadd1  8766  addext  8768  apneg  8769  nn1m1nn  9139  nn1gt1  9155  elznn0  9472  elz2  9529  nn0n0n1ge2b  9537  nneoor  9560  uztric  9756  ltxr  9983  fzsplit2  10258  uzsplit  10300  nelfzo  10360  fzospliti  10386  fzouzsplit  10389  exbtwnzlemstep  10479  exbtwnzlemex  10481  qavgle  10490  frec2uzled  10663  sq11ap  10941  swrdnd  11206  sqrt11ap  11564  abs00ap  11588  maxclpr  11748  minmax  11756  minclpr  11763  xrmaxiflemcom  11775  xrminmax  11791  xrminltinf  11798  sumeq1  11881  sumeq2  11885  fz1f1o  11901  summodc  11909  fsum3  11913  prodeq1f  12078  prodeq2w  12082  prodeq2  12083  prodmodc  12104  fprodseq  12109  fprodcl2lem  12131  zeo3  12394  odd2np1lem  12398  dvdsprime  12659  coprm  12681  ennnfonelemrnh  13002  igsumvalx  13437  gsumfzval  13439  gsumpropd  13440  gsumpropd2  13441  gsumress  13443  gsum0g  13444  islring  14171  isdomn  14248  opprdomnbg  14253  znidom  14636  reopnap  15235  dich0  15341  reapef  15467  logrpap0b  15565  wilthlem1  15669  perfectlem2  15689  lgslem1  15694  upgrm  15915  upgr1or2  15916  upgr1elem1  15935  edgupgren  15954  usgruspgrben  15999  decidi  16214  bj-nn0suc0  16368  bj-inf2vnlem2  16389  bj-nn0sucALT  16396  isomninnlem  16458  trilpolemlt1  16469  trirec0  16472