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

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

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21imbi1d 224 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 223 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 181 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  nfbidf  1448  drnf1  1637  drnf2  1638  equveli  1658  ax11v2  1717  ax11v  1724  ax11ev  1725  equs5or  1727  mobidh  1950  mobid  1951  axext3  2039  cbvralf  2544  cbvraldva2  2554  gencbval  2619  vtoclgaf  2635  vtocl2gaf  2637  vtocl3gaf  2639  rspct  2666  rspc  2667  rspc2gv  2684  ceqex  2694  ralab2  2728  mob2  2744  mob  2746  morex  2748  reu7  2759  reu8  2760  nelrdva  2769  cdeqim  2780  sbcimg  2827  csbhypf  2913  cbvralcsf  2936  dfss2f  2964  sbcssg  3358  sneqrg  3561  elintab  3654  intss1  3658  intmin  3663  dfiin2g  3718  trel  3889  trss  3891  bnd2  3954  zfpow  3956  rext  3979  opth  4002  copsexg  4009  poeq1  4064  pocl  4068  swopolem  4070  swopo  4071  soeq1  4080  sowlin  4085  frforeq2  4110  frforeq3  4112  frirrg  4115  frind  4117  weeq1  4121  ordelord  4146  reusv3i  4219  ordtriexmid  4275  ontr2exmid  4278  onsucsssucexmid  4280  onsucelsucexmid  4283  ordsucunielexmid  4284  regexmidlem1  4286  regexmid  4288  reg2exmid  4289  elirr  4294  en2lp  4306  ordsoexmid  4314  onintexmid  4325  reg3exmid  4332  tfis  4334  tfisi  4338  peano2  4346  findes  4354  nnregexmid  4370  vtoclr  4416  poinxp  4437  soinxp  4438  posng  4440  ssrel  4456  ssrel2  4458  ssrelrel  4468  relop  4514  issref  4735  iota5  4915  dffun4f  4946  sbcfung  4953  funopg  4962  brprcneu  5199  funfveu  5216  tz6.12f  5230  funbrfv  5240  ssimaexg  5263  fvmptss2  5275  fvmptssdm  5283  fvmptf  5291  fvelrn  5326  f1veqaeq  5436  dff13f  5437  isopolem  5489  isosolem  5491  riota5f  5520  oprabid  5565  ovmpt2s  5652  ov2gf  5653  ovi3  5665  caovcan  5693  caovordig  5694  caofrss  5763  caoftrn  5764  dfoprab4f  5847  f1o2ndf1  5877  poxp  5881  smoel  5946  tfrlem1  5954  nnsucelsuc  6101  nnsucsssuc  6102  nnmordi  6120  nnaordex  6131  qsel  6214  eroveu  6228  ecopovtrn  6234  ecopovtrng  6237  th3qlem2  6240  fundmeng  6318  phplem3g  6350  nneneq  6351  ssfiexmid  6367  findcard  6376  findcard2  6377  findcard2s  6378  findcard2d  6379  findcard2sd  6380  diffifi  6382  ac6sfi  6383  supeq3  6396  supeq123d  6397  supmoti  6399  suplubti  6406  supisolem  6412  ordiso2  6415  ltsonq  6554  ltexnqq  6564  prcdnql  6640  prcunqu  6641  prloc  6647  prdisj  6648  genprndl  6677  genprndu  6678  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemcl  6832  caucvgprprlemcbv  6843  caucvgprprlemval  6844  lttrsr  6905  ltsosr  6907  recexgt0sr  6916  mulgt0sr  6920  aptisr  6921  mulextsr1  6923  srpospr  6925  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  caucvgsr  6944  axprecex  7012  axpre-ltwlin  7015  axpre-lttrn  7016  axpre-apti  7017  axpre-mulgt0  7019  axpre-mulext  7020  axcaucvglemcau  7030  axcaucvglemres  7031  ltleletr  7159  squeeze0  7945  nnsub  8028  fzind  8412  uzind4s  8629  uzind4s2  8630  indstr  8632  frec2uzzd  9350  frec2uzuzd  9352  frec2uzltd  9353  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  expcl2lemap  9432  facdiv  9606  facwordi  9608  caucvgre  9808  climcn1  10060  climcn2  10061  subcn2  10063  ndvdssub  10242  sqrt2irr  10251  ialgcvg  10270  ialgcvga  10273  ialgfx  10274  cbvrald  10314  bj-bdfindes  10461  bj-omtrans  10468  bj-inf2vnlem1  10482  bj-inf2vnlem2  10483  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485  bj-findes  10493  strcoll2  10495  sscoll2  10500
  Copyright terms: Public domain W3C validator