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

Theorem orbi12d 793
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
orbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
orbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
orbi12d  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )

Proof of Theorem orbi12d
StepHypRef Expression
1 orbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21orbi1d 791 . 2  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
3 orbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43orbi2d 790 . 2  |-  ( ph  ->  ( ( ch  \/  th )  <->  ( ch  \/  ta ) ) )
52, 4bitrd 188 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    \/ wo 708
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 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm4.39  822  dcbid  838  3orbi123d  1311  dfbi3dc  1397  eueq3dc  2911  sbcor  3007  sbcorg  3008  unjust  3132  elun  3276  ifbi  3554  elprg  3611  eltpg  3636  rabrsndc  3659  preq12bg  3771  exmid01  4195  exmidsssnc  4200  swopolem  4301  soeq1  4311  sowlin  4316  ordtri2orexmid  4518  regexmidlemm  4527  regexmidlem1  4528  reg2exmidlema  4529  ordsoexmid  4557  ordtri2or2exmid  4566  ontri2orexmidim  4567  nn0suc  4599  nndceq0  4613  0elnn  4614  soinxp  4692  fununi  5279  funcnvuni  5280  fun11iun  5477  unpreima  5636  isosolem  5818  xporderlem  6225  poxp  6226  frec0g  6391  freccllem  6396  frecfcllem  6398  frecsuclem  6400  frecsuc  6401  inffiexmid  6899  fidcenumlemrk  6946  isomni  7127  enomnilem  7129  finomni  7131  exmidomni  7133  fodjuomnilemres  7139  onntri45  7233  indpi  7319  ltexprlemloc  7584  addextpr  7598  ltsosr  7741  aptisr  7756  mulextsr1lem  7757  mulextsr1  7758  axpre-ltwlin  7860  axpre-apti  7862  axpre-mulext  7865  axltwlin  8002  axapti  8005  axsuploc  8007  reapval  8510  reapti  8513  reapmul1lem  8528  reapmul1  8529  reapadd1  8530  reapneg  8531  reapcotr  8532  remulext1  8533  apreim  8537  apsym  8540  apcotr  8541  apadd1  8542  addext  8544  apneg  8545  nn1m1nn  8913  nn1gt1  8929  elznn0  9244  elz2  9300  nn0n0n1ge2b  9308  nneoor  9331  uztric  9525  ltxr  9749  fzsplit2  10023  uzsplit  10065  fzospliti  10149  fzouzsplit  10152  exbtwnzlemstep  10221  exbtwnzlemex  10223  qavgle  10232  frec2uzled  10402  sq11ap  10660  sqrt11ap  11018  abs00ap  11042  maxclpr  11202  minmax  11209  minclpr  11216  xrmaxiflemcom  11228  xrminmax  11244  xrminltinf  11251  sumeq1  11334  sumeq2  11338  fz1f1o  11354  summodc  11362  fsum3  11366  prodeq1f  11531  prodeq2w  11535  prodeq2  11536  prodmodc  11557  fprodseq  11562  fprodcl2lem  11584  zeo3  11843  odd2np1lem  11847  dvdsprime  12092  coprm  12114  ennnfonelemrnh  12387  reopnap  13671  reapef  13832  logrpap0b  13930  lgslem1  14034  decidi  14169  bj-nn0suc0  14324  bj-inf2vnlem2  14345  bj-nn0sucALT  14352  isomninnlem  14401  trilpolemlt1  14412  trirec0  14415
  Copyright terms: Public domain W3C validator