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

Theorem imbi12d 232
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 229 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 228 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 186 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  stbid  777  nfbidf  1477  drnf1  1668  drnf2  1669  equveli  1689  ax11v2  1748  ax11v  1755  ax11ev  1756  equs5or  1758  mobidh  1982  mobid  1983  axext3  2071  cbvralf  2584  cbvraldva2  2594  gencbval  2667  vtoclgaf  2684  vtocl2gaf  2686  vtocl3gaf  2688  rspct  2715  rspc  2716  rspc2gv  2732  ceqex  2742  ralab2  2777  mob2  2793  mob  2795  morex  2797  reu7  2808  reu8  2809  nelrdva  2820  cdeqim  2831  sbcimg  2878  csbhypf  2964  cbvralcsf  2988  dfss2f  3014  sbcssg  3387  sneqrg  3601  elintab  3694  intss1  3698  intmin  3703  dfiin2g  3758  disji2  3830  disjiun  3832  trel  3935  trss  3937  bnd2  4000  zfpow  4002  exmidexmid  4022  rext  4033  opth  4055  copsexg  4062  poeq1  4117  pocl  4121  swopolem  4123  swopo  4124  soeq1  4133  sowlin  4138  frforeq2  4163  frforeq3  4165  frirrg  4168  frind  4170  weeq1  4174  ordelord  4199  reusv3i  4272  ordtriexmid  4328  ontr2exmid  4331  onsucsssucexmid  4333  onsucelsucexmid  4336  ordsucunielexmid  4337  regexmidlem1  4339  regexmid  4341  reg2exmid  4342  elirr  4347  en2lp  4360  ordsoexmid  4368  onintexmid  4378  reg3exmid  4385  tfis  4388  tfisi  4392  peano2  4400  findes  4408  nnregexmid  4424  omsinds  4425  vtoclr  4474  poinxp  4495  soinxp  4496  posng  4498  ssrel  4514  ssrel2  4516  ssrelrel  4526  relop  4574  issref  4801  iota5  4987  dffun4f  5018  sbcfung  5025  funopg  5034  brprcneu  5282  funfveu  5302  tz6.12f  5317  funbrfv  5327  ssimaexg  5350  fvmptss2  5363  fvmptssdm  5371  fvmptf  5379  fvelrn  5414  f1veqaeq  5530  dff13f  5531  isopolem  5583  isosolem  5585  riota5f  5614  imbrov2fvoveq  5659  oprabid  5663  ovmpt2s  5750  ov2gf  5751  ovi3  5763  caovcan  5791  caovordig  5792  caofrss  5861  caoftrn  5862  dfoprab4f  5945  f1o2ndf1  5975  poxp  5979  smoel  6047  tfrlem1  6055  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlembfn  6091  tfr1onlemaccex  6095  tfr1onlemres  6096  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemaccex  6108  tfrcllemres  6109  tfrcl  6111  nnsucelsuc  6234  nnsucsssuc  6235  nnmordi  6255  nnaordex  6266  qsel  6349  eroveu  6363  ecopovtrn  6369  ecopovtrng  6372  th3qlem2  6375  fundmeng  6504  phplem3g  6552  nneneq  6553  ssfiexmid  6572  domfiexmid  6574  findcard  6584  findcard2  6585  findcard2s  6586  findcard2d  6587  findcard2sd  6588  diffifi  6590  ac6sfi  6594  fisseneq  6621  fidcenumlemrk  6642  fidcenumlemr  6643  isbth  6655  supeq3  6664  supeq123d  6665  supmoti  6667  suplubti  6674  supisolem  6682  cnvinfex  6692  eqinfti  6694  infvalti  6696  ordiso2  6707  isomni  6771  finomni  6775  exmidomni  6777  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  ltsonq  6936  ltexnqq  6946  prcdnql  7022  prcunqu  7023  prloc  7029  prdisj  7030  genprndl  7059  genprndu  7060  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprlemcl  7214  caucvgprprlemcbv  7225  caucvgprprlemval  7226  lttrsr  7287  ltsosr  7289  recexgt0sr  7298  mulgt0sr  7302  aptisr  7303  mulextsr1  7305  srpospr  7307  caucvgsrlemgt1  7319  caucvgsrlemoffres  7324  caucvgsr  7326  axprecex  7394  axpre-ltwlin  7397  axpre-lttrn  7398  axpre-apti  7399  axpre-mulgt0  7401  axpre-mulext  7402  axcaucvglemcau  7412  axcaucvglemres  7413  ltleletr  7546  squeeze0  8337  nnsub  8432  fzind  8831  uzind4s  9047  uzind4s2  9048  indstr  9050  supinfneg  9052  infsupneg  9053  frec2uzuzd  9774  frec2uzltd  9775  uzsinds  9813  iseqfveq2  9855  seq3fveq2  9857  iseqshft2  9863  monoord  9869  seq3split  9872  iseqsplit  9873  seq3id2  9905  iseqid2  9906  expcl2lemap  9932  facdiv  10111  facwordi  10113  zfz1isolem1  10210  zfz1iso  10211  iseqcoll  10212  caucvgre  10379  fimaxre2  10622  climcn1  10661  climcn2  10662  subcn2  10664  isummolem2a  10735  fsumsplitf  10765  fsum2d  10792  modfsummod  10815  fsumabs  10822  telfsumo  10823  fsumiun  10833  ndvdssub  11023  bezoutlemmain  11080  bezoutlemex  11083  bezoutlemzz  11084  bezoutlemsup  11091  dfgcd2  11096  ialgcvg  11123  ialgcvga  11126  ialgfx  11127  lcmgcdlem  11152  lcmdvds  11154  coprmgcdb  11163  coprmdvds1  11166  coprmdvds2  11168  prmind2  11195  dvdsprime  11197  nprm  11198  dvdsprm  11211  exprmfct  11212  coprm  11216  isprm6  11219  prmfac1  11224  sqrt2irr  11234  cbvrald  11345  bj-bdfindes  11501  bj-omtrans  11508  bj-inf2vnlem1  11522  bj-inf2vnlem2  11523  bj-inf2vnlem3  11524  bj-inf2vnlem4  11525  bj-findes  11533  strcoll2  11535  sscoll2  11540  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator