Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  orbi12d Unicode version

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
StepHypRef Expression
1 orbi12d.1 . . 3
21orbi1d 781 . 2
3 orbi12d.2 . . 3
43orbi2d 780 . 2
52, 4bitrd 187 1
 Colors of variables: wff set class 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  1290  dfbi3dc  1376  eueq3dc  2863  sbcor  2958  sbcorg  2959  unjust  3080  elun  3223  ifbi  3498  elprg  3553  eltpg  3577  rabrsndc  3600  preq12bg  3709  exmid01  4130  exmidsssnc  4135  swopolem  4236  soeq1  4246  sowlin  4251  ordtri2orexmid  4447  regexmidlemm  4456  regexmidlem1  4457  reg2exmidlema  4458  ordsoexmid  4486  ordtri2or2exmid  4495  nn0suc  4527  nndceq0  4540  0elnn  4541  soinxp  4618  fununi  5200  funcnvuni  5201  fun11iun  5397  unpreima  5554  isosolem  5734  xporderlem  6137  poxp  6138  frec0g  6303  freccllem  6308  frecfcllem  6310  frecsuclem  6312  frecsuc  6313  inffiexmid  6809  fidcenumlemrk  6852  isomni  7018  enomnilem  7020  finomni  7022  exmidomni  7024  fodjuomnilemres  7030  onntri45  7111  indpi  7194  ltexprlemloc  7459  addextpr  7473  ltsosr  7616  aptisr  7631  mulextsr1lem  7632  mulextsr1  7633  axpre-ltwlin  7735  axpre-apti  7737  axpre-mulext  7740  axltwlin  7876  axapti  7879  axsuploc  7881  reapval  8382  reapti  8385  reapmul1lem  8400  reapmul1  8401  reapadd1  8402  reapneg  8403  reapcotr  8404  remulext1  8405  apreim  8409  apsym  8412  apcotr  8413  apadd1  8414  addext  8416  apneg  8417  nn1m1nn  8782  nn1gt1  8798  elznn0  9113  elz2  9166  nn0n0n1ge2b  9174  nneoor  9197  uztric  9391  ltxr  9612  fzsplit2  9881  uzsplit  9923  fzospliti  10004  fzouzsplit  10007  exbtwnzlemstep  10076  exbtwnzlemex  10078  qavgle  10087  frec2uzled  10253  sq11ap  10509  sqrt11ap  10862  abs00ap  10886  maxclpr  11046  minmax  11053  minclpr  11060  xrmaxiflemcom  11070  xrminmax  11086  xrminltinf  11093  sumeq1  11176  sumeq2  11180  fz1f1o  11196  summodc  11204  fsum3  11208  prodeq1f  11373  prodeq2w  11377  prodeq2  11378  prodmodc  11399  fprodseq  11404  zeo3  11621  odd2np1lem  11625  dvdsprime  11859  coprm  11878  ennnfonelemrnh  11985  reopnap  12766  reapef  12927  logrpap0b  13025  decidi  13193  bj-nn0suc0  13339  bj-inf2vnlem2  13360  bj-nn0sucALT  13367  isomninnlem  13419  trilpolemlt1  13430  trirec0  13433
 Copyright terms: Public domain W3C validator