Theorem imbi12d 624

Description: Deduction joining two equivalences to form equivalence of implications.

Hypotheses

Ref	Expression
bi12d.1	|- (ph -> (ps <-> ch))
bi12d.2	|- (ph -> (th <-> ta))

Assertion

Ref	Expression
imbi12d	|- (ph -> ((ps -> th) <-> (ch -> ta)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	imbi1d 611	. 2 |- (ph -> ((ps -> th) <-> (ch -> th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	imbi2d 610	. 2 |- (ph -> ((ch -> th) <-> (ch -> ta)))
5	2, 4	bitrd 526	1 |- (ph -> ((ps -> th) <-> (ch -> ta)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  ax11v2 1210  hbsb4t 1244  ax11eq 1356  ax11el 1357  ax11inda 1364  a12lem1 1369  mobid 1397  2mo 1440  2eu6 1447  zfext2 1454  hblem 1556  ralcom2 1768  cbvralf 1788  vtoclgaf 1842  rcla4 1862  ceqex 1877  moi 1915  reu7 1925  reu8 1926  hbsbcg 1941  sbcimg 1960  sbcralt 1980  csbiegft 2019  dfss2f 2050  uniiunlem 2122  elinti 2532  elintab 2534  intss1 2538  ssintab 2540  intmin 2543  ssiun2s 2584  trel 2677  trss 2679  axpow 2733  dtruALT 2738  rext 2744  copsexg 2782  ssopab2 2811  poeq1 2833  pocl 2835  so 2855  reuuni2f 2873  fri 2908  frc 2910  efrirr 2918  ordelord 2960  tfis 3117  dfom2 3123  limomss 3127  nnlim 3134  findsg 3147  findes 3150  tfindsg 3152  tfindsg2 3153  tfindes 3154  vtoclr 3201  ralxp 3208  relop 3265  breldmg 3305  funopg 3533  fneu 3578  tz6.12f 3723  tz6.12i 3726  funbrfv 3735  funopfvg 3737  fnbrfvb 3738  fvelima 3749  ssimaexg 3754  fvelrn 3797  f1fvf 3860  f1fveq 3861  isofrlem 3886  f1oweALT 3891  tfrlem1 3896  rdglimt 3933  tz7.48lem 3940  tz7.49 3944  caoprcan 4041  oawordeu 4173  omordi 4181  oeordi 4198  nneob 4239  omsmolem 4240  ersym 4256  ertr 4258  ecopoprtrn 4295  th3qlem2 4299  ensymg 4392  xpdom2 4422  xpdom1g 4424  sbth 4437  pwen 4483  limensuc 4487  nneneq 4492  php 4493  php2 4494  pssnn 4513  unifi 4532  fiint 4534  abfii4 4538  fodomfi 4540  supmo 4550  suplub 4555  zfregcl 4567  inf0 4578  inf3lem1 4585  axinf 4595  axinf2 4596  dfom3 4602  elom3 4603  unbnnt 4611  setind 4620  r1ord 4627  rankun 4663  bnd2 4696  aceq3lem 4704  aceq5lem4 4710  aceq5 4712  aceq6b 4714  kmlem1 4737  kmlem4 4740  kmlem10 4746  kmlem12 4748  kmlem13 4749  numthlem 4755  zorn2lem7 4766  fodomg 4771  unidomg 4781  unxpdom 4816  sucxpdom 4818  alephordi 4846  alephfp 4872  dominf 4876  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem2 4927  axregnd 4928  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  zfcndpow 4940  zfcndinf 4942  indpi 5006  ltsopq 5047  ltexpq 5052  prcdpq 5069  prnmax 5071  ltsopr 5108  prlem934a 5109  ltsosr 5175  recexsrlem 5184  mulgt0sr 5186  map2psrpr 5192  suppsrlem 5193  suppsr 5194  suppsr2 5195  supsrlem6 5202  supre 5232  ltsor 5233  axrrecex 5256  pre-axmulgt0 5262  axsup 5479  msqgt0t 5589  gt0ne0t 5592  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  mulge0t 5652  mulcant 5661  divmult 5676  divclt 5681  divcan1t 5689  divcan2t 5690  recne0t 5695  recidt 5698  divrect 5702  divdirt 5713  divcan3t 5718  redivclt 5756  prodgt0t 5782  prodge0t 5784  ltmul1t 5786  ltdiv1t 5805  ltmuldivt 5817  ltrect 5832  lerect 5833  lt2msqt 5834  le2msqt 5851  squeeze0 5872  nnleltp1t 5901  nnsub 5903  infm3 6001  infmsup 6015  nnunb 6017  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrre 6030  dfuz 6150  peano5uzt 6152  uzindOLD 6156  zmax 6168  zbtwnre 6169  monoord 6231  om2uzlt 6235  ser1ft 6265  ser1add2 6275  ser1add 6276  icoun 6346  snunioo 6348  uzind4s 6384  uzind4s2 6385  nnwof 6391  fsequb 6455  seqzfveq 6486  sq11t 6560  sqrlem6 6608  sqrlem12 6614  sqrclt 6640  sqrgt0t 6641  sqrge0t 6642  sqrlet 6643  sqr00t 6644  sqrsqt 6652  sqsqrt 6653  sqr2irrlem2 6655  sqr2irrlem3 6656  absdivt 6795  absidt 6797  cjdivt 6827  abs3lemt 6844  seq1ublem 6848  cau3i 6851  cau3ir 6852  cvg2 6859  caubnd 6863  facdivt 6879  facwordit 6881  faclbnd4lem2 6886  bccl2t 6909  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  csbfsum 6965  fsumcom 6966  fsumrev 6967  fsummulc1 6971  fsumcmp 6978  fsumabs 6981  clm4le 7019  clmi1 7024  clm4at 7028  climfnn 7030  climconst3 7033  2climnn 7039  2climnn0 7040  climshft 7041  climaddlem3 7052  climmullem8 7063  climmulc2 7065  climubi 7089  climcau 7092  caucvglem2 7094  caucvg 7099  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1cmp2 7113  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  infcvgaux2 7155  expcnvlem3 7164  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem4 7188  fsum0diag 7193  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  efaddlem24 7303  efcnlem4 7362  infpn2 7452  ruclem25 7477  ruclem32 7484  istopg 7538  uniopnt 7540  tgss2t 7579  clsval2 7627  clsndisj 7648  elcls3 7652  islp2 7688  cnpval 7699  iscnp 7700  cnpimaex 7704  cncnp 7717  hausnei 7723  metcnplem 7825  metcnp 7826  metcnp2 7827  metcnpi 7829  metcnpi2 7830  metcni 7833  metcnss2 7838  cncfmet 7844  lmcvg 7870  lmle 7895  metelcls 7900  metcnp4lem2 7903  metcnp4 7904  metcn4i 7906  iscms2lem5 7927  lmcau 7930  bcthlem2 7934  bcthlem18 7950  bcth 7966  isgrp2i 8011  nvz 8236  nvcni 8266  sm1cnilem 8281  nvcnpi4 8355  nmoubi 8367  nmobndseqi 8372  nmlno0 8387  blocnilem 8395  ipdir 8433  ipass 8436  siilem2 8443  ubthi 8475  minveclem27 8502  pslem 8573  spwval2 8577  spwmo 8580  efifolem3 8639  axgroth3 8718  axgroth4 8719  grothinf 8720  normpytht 8933  norm3lemt 8940  closedsub 9014  chlim 9025  hlimcaui 9027  hlimunii 9029  ch2 9035  chcompl 9036  occllem6 9094  occllem8 9096  projlem1 9102  projlem20 9121  projlem28 9129  projlem29 9130  omlsi 9160  pjomlt 9184  h1de2 9391  elspansn2t 9406  h1datomt 9422  pjoml2t 9471  pjoml3t 9472  lecmt 9477  osumt 9505  spansncvt 9515  pjcjt2 9554  pjopytht 9582  eigret 9678  eigortht 9681  nmopubt 9749  cnopct 9753  nmfnleubt 9765  cnfnct 9770  nmcopexlem2 9867  nmcopexlem6 9871  nmcfnexlem2 9896  nmcfnexlem6 9900  nlelch 9909  hmopidmch 9990  pjssge0t 10005  hstel2t 10056  stjt 10072  str 10094  hstr 10102  stcltr1 10111  mdbrt 10131  mdit 10132  mdbr3 10134  mdbr4 10135  dmdbrt 10136  dmdmdt 10137  dmdit 10139  dmdbr3 10141  dmdbr4 10142  mdsl1 10156  mdslmd1lem3 10162  mdslmd1lem4 10163  mdslmd1 10164  csmdsym 10169  cvmdt 10171  atss 10181  atom1d 10188  chcv1t 10190  hatomict 10195  atordt 10223  atcvat2t 10224  mddmdin0 10263  ghomf1olem 10301  hmeogrp 10425  isfil 10433  fillsb 10435  fipfil2 10439  fgsb 10444  filint2 10446  cnfilca 10451  ist1 10458  isded 10513  dedi 10514  domcmpd 10523  codcmpd 10524  iscat 10531  cati 10532  cmpasso 10550  cmpida 10551  cmpidb 10552  ishomd 10562  ismona 10579  ismonb 10580  ismonb2 10582  cmpmon 10585  isfuna 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain