Theorem orbi12d 805

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.39  834  dcbid  850  ifpbi123d  1005  3orbi123d  1352  dfbi3dc  1446  eueq3dc  3000  sbcor  3096  sbcorg  3097  unjust  3223  elun  3370  elif  3652  ifbi  3661  elprg  3729  eltpg  3754  rabsnifsb  3777  rabrsndc  3779  preq12bg  3898  exmid01  4335  exmidsssnc  4340  swopolem  4450  soeq1  4460  sowlin  4465  ordtri2orexmid  4670  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  ordsoexmid  4709  ordtri2or2exmid  4718  ontri2orexmidim  4719  nn0suc  4751  nndceq0  4765  0elnn  4766  soinxp  4845  fununi  5449  funcnvuni  5450  fun11iun  5660  unpreima  5833  isosolem  6030  xporderlem  6467  poxp  6468  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  inffiexmid  7213  fidcenumlemrk  7271  isomni  7477  enomnilem  7479  finomni  7481  exmidomni  7483  fodjuomnilemres  7489  onntri45  7601  papeq1  7610  papcotr  7614  tapeq1  7619  netap  7621  2omotaplemap  7624  indpi  7710  ltexprlemloc  7975  addextpr  7989  ltsosr  8132  aptisr  8147  mulextsr1lem  8148  mulextsr1  8149  axpre-ltwlin  8251  axpre-apti  8253  axpre-mulext  8256  axltwlin  8394  axapti  8397  axsuploc  8399  reapval  8907  reapti  8910  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  reapneg  8928  reapcotr  8929  remulext1  8930  apreim  8934  apsym  8937  apcotr  8938  apadd1  8939  addext  8941  apneg  8942  nn1m1nn  9325  nn1gt1  9341  elznn0  9664  elz2  9721  nn0n0n1ge2b  9730  nneoor  9753  uztric  9954  ltxr  10188  fzsplit2  10466  fzsplit3  10469  uzsplit  10510  nelfzo  10570  fzospliti  10596  fzouzsplit  10599  exbtwnzlemstep  10693  exbtwnzlemex  10695  qavgle  10704  frec2uzled  10881  sq11ap  11160  swrdnd  11447  sqrt11ap  11820  abs00ap  11844  maxclpr  12005  minmax  12014  minclpr  12021  xrmaxiflemcom  12034  xrminmax  12050  xrminltinf  12057  sumeq1  12140  sumeq2  12144  fz1f1o  12160  summodc  12169  fsum3  12173  prodeq1f  12338  prodeq2w  12342  prodeq2  12343  prodmodc  12364  fprodseq  12369  fprodcl2lem  12391  zeo3  12654  odd2np1lem  12658  dvdsprime  12919  coprm  12942  ennnfonelemrnh  13359  gzsumvalx  13762  gzsumfzval  13764  gzsumress  13765  gzsum0  13766  islring  14583  opprlring  14588  isdomn  14662  opprdomnbg  14667  znidom  15076  reopnap  15738  dich0  15844  reapef  15970  logrpap0b  16070  zprmlogbap  16179  wilthlem1  16193  perfectlem2  16261  prmefexple  16269  bposlem1  16272  lgslem1  16285  upgrm  16507  upgr1or2  16508  upgr1elem1  16527  edgupgren  16548  usgruspgrben  16593  subupgr  16680  konigsberglem1  16895  dichmul0orlem3  16921  dichmul0orlem7  16925  decidi  16989  bj-nn0suc0  17142  bj-inf2vnlem2  17163  bj-nn0sucALT  17170  wexmiddc  17208  isomninnlem  17245  trilpolemlt1  17257  trirec0  17260