Theorem imbi12d 626

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 613	. 2 |- (ph -> ((ps -> th) <-> (ch -> th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	imbi2d 612	. 2 |- (ph -> ((ch -> th) <-> (ch -> ta)))
5	2, 4	bitrd 528	1 |- (ph -> ((ps -> th) <-> (ch -> ta)))

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

This theorem is referenced by:  ax11v2 1215  hbsb4t 1249  ax11eq 1363  ax11el 1364  ax11inda 1371  a12lem1 1376  mobid 1404  2mo 1447  2eu6 1454  zfext2 1461  hblem 1564  ralcom2 1776  cbvralf 1796  vtoclgaf 1851  rcla4 1871  ceqex 1886  moi2 1924  moi 1925  reu7 1935  reu8 1936  hbsbcg 1951  sbcimg 1970  sbcralt 1990  csbiegft 2029  dfss2f 2060  uniiunlem 2132  elinti 2542  elintab 2544  intss1 2548  ssintab 2550  intmin 2553  ssiun2s 2594  trel 2687  trss 2689  axpow 2743  dtruALT 2748  rext 2754  copsexg 2792  ssopab2 2822  poeq1 2842  pocl 2844  so 2864  reuuni2f 2883  fri 2918  frc 2920  efrirr 2928  ordelord 2970  tfis 3127  dfom2 3133  limomss 3137  nnlim 3144  findsg 3157  findes 3160  tfindsg 3162  tfindsg2 3163  tfindes 3164  vtoclr 3211  ralxp 3218  relop 3275  breldmg 3316  funopg 3547  fneu 3592  tz6.12f 3738  tz6.12i 3741  funbrfv 3750  funopfvg 3752  fnbrfvb 3753  fvelima 3764  ssimaexg 3769  fvelrn 3812  f1fvf 3875  f1fveq 3876  isofrlem 3901  f1oweALT 3906  tfrlem1 3911  rdglimt 3948  tz7.48lem 3955  tz7.49 3959  caoprcan 4055  oawordeu 4189  omordi 4197  oeordi 4214  nneob 4255  omsmolem 4256  ersym 4272  ertr 4274  ecopoprtrn 4311  th3qlem2 4315  ensymg 4411  xpdom2 4442  xpdom1g 4444  sbth 4457  pwen 4503  limensuc 4507  nneneq 4512  php 4513  php2 4514  pssnn 4534  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii4OLD 4564  fodomfiOLD 4566  supmo 4576  suplub 4581  zfregcl 4595  inf0 4606  inf3lem1 4613  axinf 4623  axinf2 4624  dfom3 4630  elom3 4631  unbnnt 4639  setind 4648  r1ord 4655  rankun 4691  bnd2 4724  aceq3lem 4732  aceq5lem4 4738  aceq5 4740  aceq6b 4742  kmlem1 4765  kmlem4 4768  kmlem10 4774  kmlem12 4776  kmlem13 4777  numthlem 4783  zorn2lem7 4794  fodomg 4799  unidomg 4809  unxpdom 4844  sucxpdom 4846  alephordi 4874  alephfp 4900  dominf 4904  axrepndlem1 4944  axrepndlem2 4945  axunndlem1 4947  axunnd 4948  axpowndlem2 4950  axpowndlem3 4951  axpowndlem4 4952  axregndlem2 4955  axregnd 4956  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964  zfcndpow 4968  zfcndinf 4970  indpi 5034  ltsopq 5075  ltexpq 5080  prcdpq 5097  prnmax 5099  ltsopr 5136  prlem934a 5137  ltsosr 5203  recexsrlem 5212  mulgt0sr 5214  map2psrpr 5220  suppsrlem 5221  suppsr 5222  suppsr2 5223  supsrlem6 5230  supre 5260  ltsor 5261  axrrecex 5284  pre-axmulgt0 5290  axsup 5507  msqgt0t 5615  gt0ne0t 5618  lt2addt 5643  le2addt 5644  addgt0t 5647  addgegt0t 5648  addge0t 5650  mulge0t 5679  mulcant 5690  mulcantOLD 5691  divmult 5707  divclt 5712  divcan1t 5724  divcan1tOLD 5725  divcan2tOLD 5727  recne0t 5732  recidt 5735  divrect 5739  divdirt 5750  divdirtOLD 5751  divcan3t 5760  divcan3tOLD 5761  redivclt 5800  prodgt0t 5826  prodge0t 5828  ltmul1t 5830  ltdiv1t 5849  ltdiv1tOLD 5850  ltmuldivt 5863  ltmuldivtOLD 5864  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  squeeze0 5924  nnleltp1t 5954  nnsub 5956  infm3 6054  infmsup 6068  nnunb 6070  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrre 6083  dfuz 6202  peano5uzt 6204  uzindOLD 6208  zmax 6220  zbtwnre 6221  monoord 6294  om2uzlt 6298  ser1ft 6328  ser1add2 6338  ser1add 6339  icoun 6413  snunioo 6415  uzind4s 6452  uzind4s2 6453  nnwof 6459  fsequb 6523  seqzfveq 6554  sq11t 6629  sqrlem6 6678  sqrlem12 6684  sqrclt 6710  sqrgt0t 6711  sqrge0t 6712  sqrlet 6713  sqr00t 6714  sqrsqt 6722  sqsqrt 6723  sqr2irrlem2 6725  sqr2irrlem3 6726  absdivt 6860  absidt 6862  cjdivt 6889  abs3lemt 6907  seq1ublem 6911  cau3i 6914  cau3ir 6915  cvg2 6922  caubnd 6926  facdivt 6942  facwordit 6944  faclbnd4lem2 6949  bccl2t 6971  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  csbfsum 7027  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumcmp 7040  fsumabs 7043  clm4le 7081  clmi1 7086  clm4at 7090  climfnn 7092  climconst3 7096  2climnn 7102  2climnn0 7103  climshft 7104  climaddlem3 7116  climmullem8 7127  climmulc2 7129  climubi 7153  climcau 7156  caucvglem2 7158  caucvg 7163  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1cmp2 7177  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  infcvgaux2 7220  expcnvlem3 7229  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem4 7253  fsum0diag 7258  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  efaddlem24 7361  efcnlem4 7422  infpn2 7509  ruclem25 7534  ruclem32 7541  istopg 7596  uniopnt 7598  tgss2t 7637  clsval2 7685  clsndisj 7706  elcls3 7711  islp2 7747  cnpval 7759  iscnp 7760  cnpimaex 7765  cncnp 7778  hausnei 7784  metcnplem 7886  metcnp 7887  metcnp2 7888  metcnpi 7890  metcnpi2 7891  metcni 7894  metcnss2 7899  cncfmet 7905  lmcvg 7932  iscaunns 7944  lmle 7960  metelcls 7965  metcnp4lem2 7969  metcnp4 7970  metcn4i 7972  iscms2lem5 7993  lmcau 7996  bcthlem2 8000  bcthlem18 8016  bcth 8032  isgrp2i 8076  nvz 8297  nvcni 8329  nvcni2 8330  nvcni3 8331  sm1cnilem 8347  nvcnpi3 8422  nvcnpi4 8423  nmoubi 8435  nmobndseqi 8440  nmlno0 8455  blocnilem 8464  ipdir 8502  ipass 8505  siilem2 8512  ubthi 8544  minveclem27 8571  pslem 8647  spwval2 8653  spwmo 8656  efifolem3 8724  axgroth3 8779  axgroth4 8780  grothinf 8781  normpytht 9012  norm3lemt 9019  closedsub 9093  chlim 9104  hlimcaui 9106  hlimunii 9108  ch2 9114  chcompl 9115  occllem6 9178  occllem8 9180  projlem1 9186  projlem20 9205  projlem28 9213  projlem29 9214  omlsi 9245  pjomlt 9269  h1de2 9476  elspansn2t 9490  h1datomt 9505  pjoml2t 9554  pjoml3t 9555  lecmt 9560  osumt 9588  spansncvt 9598  pjcjt2 9637  pjopytht 9665  eigret 9761  eigortht 9764  nmopubt 9832  cnopct 9837  nmfnleubt 9849  cnfnct 9854  nmcopexlem2 9952  nmcopexlem6 9956  nmcfnexlem2 9981  nmcfnexlem6 9985  nlelch 9994  hmopidmch 10079  pjssge0t 10094  hstel2t 10146  stjt 10162  str 10184  hstr 10192  stcltr1 10201  mdbrt 10221  mdit 10222  mdbr3 10224  mdbr4 10225  dmdbrt 10226  dmdmdt 10227  dmdit 10229  dmdbr3 10232  dmdbr4 10233  dmdbr5 10235  mdsl1 10248  mdslmd1lem3 10254  mdslmd1lem4 10255  mdslmd1 10256  csmdsym 10261  cvmdt 10263  atss 10273  atom1d 10280  chcv1t 10282  hatomict 10287  atordt 10315  atcvat2t 10316  mddmdin0 10358  ghomf1olem 10396  hmeogrp 10538  isfil 10558  fillsb 10560  fipfil2 10564  fipfil2OLD 10565  fgsb 10570  fgsbOLD 10571  filint2 10574  filint2OLD 10575  cnfilca 10583  cnfilcaOLD 10584  limfillem2OLD 10608  ist1 10614  isded 10669  dedi 10670  domcmpd 10679  codcmpd 10680  iscat 10687  cati 10688  cmpasso 10706  cmpida 10707  cmpidb 10708  ishomd 10718  ismona 10737  ismonb 10738  ismonb2 10740  cmpmon 10743  isepia 10747  isepib 10748  isepib2 10750  isfuna 10754

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