Theorem imbi12d 233

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

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	imbi1d 230	. 2 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	imbi2d 229	. 2 |- ( ph -> ( ( ch -> th ) <-> ( ch -> ta ) ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  822  nfbidf  1526  drnf1  1720  drnf2  1721  equveli  1746  ax11v2  1807  ax11v  1814  ax11ev  1815  equs5or  1817  mobidh  2047  mobid  2048  axext3  2147  cbvralfw  2681  cbvralf  2682  cbvralvw  2693  cbvraldva2  2696  gencbval  2769  vtoclgaf  2786  vtocl2gaf  2788  vtocl3gaf  2790  rspct  2818  rspc  2819  rspc2gv  2837  ceqex  2848  ralab2  2885  mob2  2901  mob  2903  morex  2905  reu7  2916  reu8  2917  nelrdva  2928  cdeqim  2939  sbcimg  2987  csbhypf  3078  cbvralcsf  3102  dfss2f  3128  sbcssg  3513  sneqrg  3736  elintab  3829  intss1  3833  intmin  3838  dfiin2g  3893  disji2  3969  disjiun  3971  trel  4081  trss  4083  bnd2  4146  zfpow  4148  exmidexmid  4169  exmidsssnc  4176  exmidundifim  4180  rext  4187  opth  4209  copsexg  4216  poeq1  4271  pocl  4275  swopolem  4277  swopo  4278  soeq1  4287  sowlin  4292  frforeq2  4317  frforeq3  4319  frirrg  4322  frind  4324  weeq1  4328  ordelord  4353  reusv3i  4431  ordtriexmid  4492  ontr2exmid  4496  onsucsssucexmid  4498  onsucelsucexmid  4501  ordsucunielexmid  4502  regexmidlem1  4504  regexmid  4506  reg2exmid  4507  elirr  4512  en2lp  4525  ordsoexmid  4533  onintexmid  4544  reg3exmid  4551  tfis  4554  tfisi  4558  peano2  4566  findes  4574  nnregexmid  4592  omsinds  4593  vtoclr  4646  poinxp  4667  soinxp  4668  posng  4670  ssrel  4686  ssrel2  4688  ssrelrel  4698  relop  4748  issref  4980  iota5  5167  dffun4f  5198  sbcfung  5206  funopg  5216  brprcneu  5473  funfveu  5493  tz6.12f  5509  funbrfv  5519  ssimaexg  5542  fvmptss2  5555  fvmptssdm  5564  fvmptf  5572  fvelrn  5610  f1veqaeq  5731  dff13f  5732  isopolem  5784  isosolem  5786  riota5f  5816  imbrov2fvoveq  5861  oprabid  5865  ovmpos  5956  ov2gf  5957  ovi3  5969  caovcan  5997  caovordig  5998  caofrss  6068  caoftrn  6069  dfoprab4f  6153  f1o2ndf1  6187  poxp  6191  smoel  6259  tfrlem1  6267  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemaccex  6307  tfr1onlemres  6308  tfrcllemsucfn  6312  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllembfn  6316  tfrcllemaccex  6320  tfrcllemres  6321  tfrcl  6323  nnsucelsuc  6450  nnsucsssuc  6451  nnmordi  6475  nnaordex  6486  qsel  6569  eroveu  6583  ecopovtrn  6589  ecopovtrng  6592  th3qlem2  6595  ixpsnf1o  6693  fundmeng  6764  phplem3g  6813  nneneq  6814  ssfiexmid  6833  domfiexmid  6835  findcard  6845  findcard2  6846  findcard2s  6847  findcard2d  6848  findcard2sd  6849  diffifi  6851  ac6sfi  6855  fiintim  6885  fisseneq  6888  fidcenumlemrk  6910  fidcenumlemr  6911  isbth  6923  supeq3  6946  supeq123d  6947  supmoti  6949  suplubti  6956  supisolem  6964  cnvinfex  6974  eqinfti  6976  infvalti  6978  ordiso2  6991  nnnninfeq2  7084  isomni  7091  finomni  7095  exmidomni  7097  ctssexmid  7105  ismkv  7108  ismkvnex  7110  mkvprop  7113  fodjumkvlemres  7114  enmkvlem  7116  iswomni  7120  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  ccfunen  7196  ltsonq  7330  ltexnqq  7340  prcdnql  7416  prcunqu  7417  prloc  7423  prdisj  7424  genprndl  7453  genprndu  7454  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemcl  7608  caucvgprprlemcbv  7619  caucvgprprlemval  7620  suplocexprlemloc  7653  lttrsr  7694  ltsosr  7696  recexgt0sr  7705  mulgt0sr  7710  aptisr  7711  mulextsr1  7713  srpospr  7715  caucvgsrlemgt1  7727  caucvgsrlemoffres  7732  caucvgsr  7734  map2psrprg  7737  suplocsrlemb  7738  axprecex  7812  axpre-ltwlin  7815  axpre-lttrn  7816  axpre-apti  7817  axpre-mulgt0  7819  axpre-mulext  7820  axcaucvglemcau  7830  axcaucvglemres  7831  axpre-suploclemres  7833  axpre-suploc  7834  axsuploc  7962  ltleletr  7971  ltordlem  8371  squeeze0  8790  sup3exmid  8843  nnsub  8887  fzind  9297  uzind4s  9519  uzind4s2  9520  indstr  9522  supinfneg  9524  infsupneg  9525  frec2uzuzd  10327  frec2uzltd  10328  uzsinds  10367  seq3fveq2  10394  seq3shft2  10398  monoord  10401  seq3split  10404  seq3id2  10434  expcl2lemap  10457  nn0ltexp2  10612  facdiv  10640  facwordi  10642  zfz1isolem1  10739  zfz1iso  10740  seq3coll  10741  caucvgre  10909  fimaxre2  11154  climcn1  11235  climcn2  11236  subcn2  11238  summodclem2a  11308  fsumsplitf  11335  fsum2d  11362  modfsummod  11385  fsumabs  11392  telfsumo  11393  fsumiun  11404  prodfdivap  11474  fprod2d  11550  fproddivapf  11558  fprodsplitf  11559  fprodsplit1f  11561  ndvdssub  11852  bezoutlemmain  11916  bezoutlemex  11919  bezoutlemzz  11920  bezoutlemsup  11927  dfgcd2  11932  algcvg  11959  algcvga  11962  algfx  11963  lcmgcdlem  11988  lcmdvds  11990  coprmgcdb  11999  coprmdvds1  12002  coprmdvds2  12004  prmind2  12031  dvdsprime  12033  nprm  12034  dvdsprm  12048  exprmfct  12049  coprm  12053  isprm6  12056  prmfac1  12061  sqrt2irr  12071  pcqmul  12212  pcqcl  12215  pc2dvds  12238  pcz  12240  ennnfonelemim  12294  exmidunben  12296  uniopn  12540  fiinopn  12543  epttop  12631  cnpval  12739  iscnp  12740  icnpimaex  12752  lmcvg  12758  cnptoprest  12780  cnptoprest2  12781  lmss  12787  lmff  12790  txcnp  12812  txlm  12820  cnmpt12  12828  cnmpt22  12835  blssps  12968  blss  12969  metss  13035  comet  13040  metcnp3  13052  metcnp2  13054  txmetcnp  13059  divcnap  13096  elcncf2  13102  cncfi  13106  mulc1cncf  13117  cncfmet  13120  mulcncflem  13131  mulcncf  13132  dedekindeulemloc  13138  dedekindeulemlu  13140  dedekindeulemeu  13141  suplociccreex  13143  dedekindicclemloc  13147  dedekindicclemlu  13149  dedekindicclemeu  13150  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemloc  13160  limccl  13169  ellimc3apf  13170  limccnpcntop  13185  limccnp2lem  13186  limccoap  13188  dvcoapbr  13212  cbvrald  13504  bj-bdfindes  13666  bj-omtrans  13673  bj-inf2vnlem1  13687  bj-inf2vnlem2  13688  bj-inf2vnlem3  13689  bj-inf2vnlem4  13690  bj-findes  13698  strcoll2  13700  sscoll2  13705  exmid1stab  13714  subctctexmid  13715  pw1nct  13717  exmidsbthrlem  13735  sbthom  13739  apdiff  13761  ismkvnnlem  13765  nconstwlpolem  13777  neapmkv  13780