Theorem imbi12d 629

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

Hypotheses

Ref	Expression
bi12d.1	⊢ (φ → (ψ ↔ χ))
bi12d.2	⊢ (φ → (θ ↔ τ))

Assertion

Ref	Expression
imbi12d	⊢ (φ → ((ψ → θ) ↔ (χ → τ)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	imbi1d 616	. 2 ⊢ (φ → ((ψ → θ) ↔ (χ → θ)))
3		bi12d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	imbi2d 615	. 2 ⊢ (φ → ((χ → θ) ↔ (χ → τ)))
5	2, 4	bitrd 531	1 ⊢ (φ → ((ψ → θ) ↔ (χ → τ)))

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  ax11v2 1252  hbsb4t 1287  ax11eq 1402  ax11el 1403  ax11inda 1410  a12lem1 1415  mobid 1443  2mo 1487  2eu6 1494  axext3 1502  hblem 1607  ralcom2 1822  cbvralf 1842  vtoclgaf 1897  rcla4 1917  ceqex 1932  moi2 1970  moi 1971  reu7 1981  reu8 1982  hbsbcg 1996  sbcimg 2018  sbcralt 2040  csbiegft 2081  dfss2f 2112  uniiunlem 2184  elinti 2609  elintab 2611  intss1 2615  ssintab 2617  intmin 2620  ssiun2s 2662  trel 2761  trss 2763  zfpow 2819  el 2822  dtru 2831  rext 2834  copsexg 2868  ssopab2 2900  poeq1 2920  pocl 2922  posn 2928  so 2943  fri 2948  frc 2950  efrirr 2957  ordelord 2997  reuuni2f 3107  tfis 3208  tfindsg 3213  tfindsg2 3214  tfindes 3215  dfom2 3220  limomss 3224  nnlim 3231  findsg 3245  findes 3248  vtoclr 3294  ralxp 3301  relop 3365  breldmg 3407  funopg 3652  fneu 3698  tz6.12f 3849  tz6.12i 3852  funbrfv 3861  funopfvg 3863  fnbrfvb 3864  fvelima 3875  ssimaexg 3880  fvelrn 3926  dff13f 3989  f1fveq 3990  isofrlem 4015  f1oweALT 4020  caoprcan 4116  onfununi 4209  tfrlem1 4212  rdglim 4249  tz7.48lem 4256  tz7.49 4260  oawordeu 4325  omordi 4333  oeordi 4350  nneob 4395  omsmolem 4396  ersym 4412  ertr 4414  ecopoprtrn 4452  th3qlem2 4456  ensymg 4552  xpdom2 4583  xpdom1g 4585  ac6sfilem1 4588  ac6sfilem3 4590  ac6sfi 4591  sbth 4602  pwen 4650  limensuc 4654  nneneq 4659  php 4660  php2 4661  pssnn 4681  xpfi 4685  unifi 4701  fiint 4703  abfii4 4707  fodomfi 4709  supmo 4719  suplub 4724  zfregcl 4738  inf0 4751  inf3lem1 4758  zfinf 4768  axinf2 4769  dfom3 4776  elom3 4777  unbnn3 4785  setind 4794  r1ord 4801  rankun 4837  bnd2 4870  aceq3lem 4878  aceq5lem4 4884  aceq5 4886  aceq6b 4888  kmlem1 4911  kmlem4 4914  kmlem10 4920  kmlem12 4922  kmlem13 4923  numthlem 4929  zorn2lem7 4940  fodomg 4945  unidomg 4955  unxpdom 4994  sucxpdom 4996  alephordi 5024  alephfp 5050  dominf 5054  cdaung 5073  cdaeng 5076  axrepndlem1 5098  axrepndlem2 5099  axunndlem1 5101  axunnd 5102  axpowndlem2 5104  axpowndlem3 5105  axpowndlem4 5106  axregndlem2 5109  axregnd 5110  axinfndlem1 5111  axinfnd 5112  axacndlem4 5116  axacndlem5 5117  axacnd 5118  zfcndpow 5122  zfcndinf 5124  indpi 5188  ltsopq 5229  ltexpq 5234  prcdpq 5251  prnmax 5253  ltsopr 5290  prlem934a 5291  ltsosr 5357  recexsrlem 5366  mulgt0sr 5368  map2psrpr 5374  suppsrlem 5375  suppsr 5376  suppsr2 5377  supsrlem6 5384  supre 5414  ltsor 5415  axrrecex 5438  pre-axmulgt0 5444  axsup 5661  msqgt0 5769  gt0ne0 5772  lt2add 5797  le2add 5798  addgt0 5801  addgegt0 5802  addge0 5804  mulge0 5833  mulge0OLD 5834  mulcan 5844  divmul 5859  divcl 5864  divcan1 5872  recne0 5878  recid 5881  divrec 5885  divdir 5896  divcan3 5901  redivcl 5940  prodgt0 5966  prodge0 5968  ltmul1 5970  ltdiv1 5993  ltdiv1OLD 5994  ltmuldiv 6007  ltmuldivOLD 6008  ltrec 6029  lerec 6030  lt2msq 6031  le2msq 6048  squeeze0 6069  nnleltp1 6100  nnsubi 6102  infm3 6222  infmsup 6236  nnunb 6238  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxrre 6251  dfuzi 6373  peano5uzti 6375  uzindOLD 6379  zmax 6392  zbtwnre 6393  monoord 6482  icoun 6540  snunioo 6542  uzind4s 6579  uzind4s2 6580  nnwof 6586  fsequb 6654  om2uzlti 6661  ser1f 6693  ser1add2i 6703  ser1addi 6704  seqzfveq 6749  sq11 6826  sqrlem6 6879  sqrlem12 6885  sqrcl 6911  sqrgt0 6912  sqrge0 6913  sqrle 6914  sqr00 6915  sqrsq 6923  sqsqr 6924  sqr2irrlem2 6926  sqr2irrlem3 6927  absdiv 7062  absid 7064  cjdiv 7092  abs3lem 7110  seq1ublem 7114  cau3ii 7117  cau3iri 7118  cvg2i 7125  caubndi 7129  facdiv 7145  facwordi 7147  faclbnd4lem2 7152  bccl2 7174  fsumcllem 7217  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  csbfsum 7230  fsumcom 7231  fsumrev 7232  fsummulc1 7236  fsumcmp 7243  fsumabs 7246  clm4lei 7284  clmi1i 7289  clm4a 7293  climfnn 7295  climconst3 7299  2climnn 7305  2climnn0 7306  climshfti 7307  climaddlem3 7319  climmullem8 7330  climmulc2 7332  climubii 7356  climcaui 7359  caucvglem2 7361  caucvgi 7366  caucvg3 7371  serzf0i 7372  ser1cmp2i 7380  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  infcvgaux2i 7424  expcnvlem3 7433  cvgratlem1ALT 7452  cvgratlem1 7455  cvgratlem4 7458  fsum0diag 7463  ivthlem6 7491  ivthlem7 7492  ivthlem8 7493  efaddlem24 7566  efcnlem4 7630  infpn2 7721  ruclem25 7746  ruclem32 7753  istopg 7808  uniopn 7810  tgss2 7849  clsval2 7895  clsndisj 7916  elcls3 7921  islp2 7957  cnpval 7969  iscnp 7970  cnpimaex 7975  cncnp 7988  hausnei 7994  metcnplem 8097  metcnp 8098  metcnp2 8099  metcnpi 8101  metcnpi2 8102  metcni 8105  metcnss2 8110  cncfmet 8116  lmcvg 8143  iscaunns 8155  lmle 8171  metelcls 8176  metcnp4lem2 8180  metcnp4 8181  metcn4i 8183  iscms2lem5 8204  lmcau 8207  bcthlem2 8211  bcthlem18 8227  bcth 8243  isgrp2i 8293  nvz 8544  nvcni 8576  nvcni2 8577  nvcni3 8578  vacnlem3 8584  vacnlem4 8585  sm1cnilem 8601  nvcnpi3 8676  nvcnpi4 8677  nmoubi 8689  nmobndseqi 8695  nmlno0 8710  blocnilem 8719  ipdir 8758  ipass 8761  siilem2 8768  ubthi 8804  minveclem27 8831  pslem 8909  spwval2 8915  spwmo 8918  efifolem3 8996  axgroth3 9051  axgroth4 9052  grothinf 9053  normpyth 9288  norm3lemt 9295  closedsub 9369  chlimi 9380  hlimcauii 9382  hlimuniii 9384  ch2 9390  chcompl 9391  occllem6 9454  occllem8 9456  projlem1 9462  projlem20 9481  projlem28 9489  projlem29 9490  omlsii 9521  pjoml 9545  h1de2i 9752  elspansn2 9766  h1datom 9781  pjoml2 9830  pjoml3 9831  lecm 9836  osum 9866  spansncv 9876  pjcjt2 9915  pjopyth 9943  eigre 10041  eigorth 10044  nmopub 10112  cnopc 10117  nmfnleub 10129  cnfnc 10134  nmcopexlem2 10231  nmcopexlem6 10235  nmcfnexlem2 10260  nmcfnexlem6 10264  nlelchi 10273  hmopidmchi 10359  pjssge0i 10374  hstel2 10427  stj 10443  stri 10465  hstri 10473  stcltr1i 10482  mdbr 10502  mdi 10503  mdbr3 10505  mdbr4 10506  dmdbr 10507  dmdmd 10508  dmdi 10510  dmdbr3 10513  dmdbr4 10514  dmdbr5 10516  mdsl1i 10529  mdslmd1lem3 10535  mdslmd1lem4 10536  mdslmd1i 10537  csmdsymi 10542  cvmd 10544  atss 10554  atom1d 10561  chcv1 10563  hatomic 10568  atord 10597  atcvat2 10598  mddmdin0i 10640  ghomf1olem 10681  ref3w 10772  ac6sg 10803  inposet 10868  isass 10890  ismgm 10897  isexid2 10901  isppm 10917  unmnd 10951  fora2 10953  osneisi 11018  hmeogrp 11044  isfil 11071  fillsb 11073  fipfil2 11077  fgsb 11082  filint2 11084  cnfilca 11088  limfillem2 11102  ist1 11106  iscomp 11114  bwt2 11123  isded 11190  dedi 11191  domcmpd 11200  codcmpd 11201  iscat 11208  cati 11209  cmpasso 11227  cmpida 11228  cmpidb 11229  ishomd 11245  ismona 11264  ismonb 11265  ismonb2 11267  cmpmon 11270  isepia 11274  isepib 11275  isepib2 11277  isfuna 11288  efp2 11321  subtr 11395  subtr2 11396  dfiin2g 11400  trer 11409  finsschain 11425  ordiso 11426  ordtypelem5 11431  ordtypelem6 11432  ordtype 11434  elomsubsd 11446  omsubinit 11451  cncls 11473  cnntr 11474  compcov 11486  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  connsub 11502  1stcclb 11532  2ndc1stc 11538  comppfsc 11578  fnejoin2 11592  t0dist 11602  ist1-2 11603  ist1-3 11604  t1sep 11607  regsep 11611  nrmsep 11615  nrmsep2 11616  fbssint 11626  isufil2 11650  ufilmax 11653  ufilen 11664  flimopn 11679  limfilcf 11683  hausfillim 11685  cnpfillim 11686  rnelfm 11699  fmfnfmlem4 11703  fclusnei 11719  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomplem 11732  fcluscomp 11733  ufcomp 11734  fclusfnei 11738  dirtr 11753  morex 11804  oprabopabf 11807  erthdmg 11824  dif1en 11833  dif1card 11835  findcard 11836  fimax 11837  fimaxg 11838  acdcg 11842  acdc3g 11843  acdc5g 11844  indexf 11847  inficl 11849  supclt 11854  supubt 11855  add20 11858  eluzadd 11860  eluzsub 11861  sdc 11877  fsum00 11883  fsumlt 11884  fsumltisum 11887  fsumleisum 11890  iserzshft2 11892  mettrifi 11912  lmclim2 11915  caushft 11916  cncfco 11948  cncfres 11956  lmtlm 11969  txcn 11979  txcnoprab 11981  sstotbnd 11992  heiborlem1 12011  heiborlem9 12019  heiborlem13 12023  heiborlem16 12026  heiborlem18 12028  heiborlem36 12046  bfplem8 12061  bfp 12065

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 145  df-an 223

Copyright terms: Public domain