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  827  nfbidf  1532  drnf1  1726  drnf2  1727  equveli  1752  ax11v2  1813  ax11v  1820  ax11ev  1821  equs5or  1823  mobidh  2053  mobid  2054  axext3  2153  cbvralfw  2687  cbvralf  2689  cbvralvw  2700  cbvraldva2  2703  gencbval  2778  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  rspct  2827  rspc  2828  rspc2gv  2846  ceqex  2857  ralab2  2894  mob2  2910  mob  2912  morex  2914  reu7  2925  reu8  2926  nelrdva  2937  cdeqim  2948  sbcimg  2996  csbhypf  3087  cbvralcsf  3111  dfss2f  3138  sbcssg  3524  sneqrg  3749  elintab  3842  intss1  3846  intmin  3851  dfiin2g  3906  disji2  3982  disjiun  3984  trel  4094  trss  4096  bnd2  4159  zfpow  4161  exmidexmid  4182  exmidsssnc  4189  exmidundifim  4193  rext  4200  opth  4222  copsexg  4229  poeq1  4284  pocl  4288  swopolem  4290  swopo  4291  soeq1  4300  sowlin  4305  frforeq2  4330  frforeq3  4332  frirrg  4335  frind  4337  weeq1  4341  ordelord  4366  reusv3i  4444  ordtriexmid  4505  ontr2exmid  4509  onsucsssucexmid  4511  onsucelsucexmid  4514  ordsucunielexmid  4515  regexmidlem1  4517  regexmid  4519  reg2exmid  4520  elirr  4525  en2lp  4538  ordsoexmid  4546  onintexmid  4557  reg3exmid  4564  tfis  4567  tfisi  4571  peano2  4579  findes  4587  nnregexmid  4605  omsinds  4606  vtoclr  4659  poinxp  4680  soinxp  4681  posng  4683  ssrel  4699  ssrel2  4701  ssrelrel  4711  relop  4761  issref  4993  iota5  5180  dffun4f  5214  sbcfung  5222  funopg  5232  brprcneu  5489  funfveu  5509  tz6.12f  5525  funbrfv  5535  ssimaexg  5558  fvmptss2  5571  fvmptssdm  5580  fvmptf  5588  fvelrn  5627  f1veqaeq  5748  dff13f  5749  isopolem  5801  isosolem  5803  riota5f  5833  imbrov2fvoveq  5878  oprabid  5885  ovmpos  5976  ov2gf  5977  ovi3  5989  caovcan  6017  caovordig  6018  caofrss  6085  caoftrn  6086  dfoprab4f  6172  f1o2ndf1  6207  poxp  6211  smoel  6279  tfrlem1  6287  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  nnsucelsuc  6470  nnsucsssuc  6471  nnmordi  6495  nnaordex  6507  qsel  6590  eroveu  6604  ecopovtrn  6610  ecopovtrng  6613  th3qlem2  6616  ixpsnf1o  6714  fundmeng  6785  phplem3g  6834  nneneq  6835  ssfiexmid  6854  domfiexmid  6856  findcard  6866  findcard2  6867  findcard2s  6868  findcard2d  6869  findcard2sd  6870  diffifi  6872  ac6sfi  6876  fiintim  6906  fisseneq  6909  fidcenumlemrk  6931  fidcenumlemr  6932  isbth  6944  supeq3  6967  supeq123d  6968  supmoti  6970  suplubti  6977  supisolem  6985  cnvinfex  6995  eqinfti  6997  infvalti  6999  ordiso2  7012  nnnninfeq2  7105  isomni  7112  finomni  7116  exmidomni  7118  ctssexmid  7126  ismkv  7129  ismkvnex  7131  mkvprop  7134  fodjumkvlemres  7135  enmkvlem  7137  iswomni  7141  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  ccfunen  7226  ltsonq  7360  ltexnqq  7370  prcdnql  7446  prcunqu  7447  prloc  7453  prdisj  7454  genprndl  7483  genprndu  7484  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemcl  7638  caucvgprprlemcbv  7649  caucvgprprlemval  7650  suplocexprlemloc  7683  lttrsr  7724  ltsosr  7726  recexgt0sr  7735  mulgt0sr  7740  aptisr  7741  mulextsr1  7743  srpospr  7745  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  caucvgsr  7764  map2psrprg  7767  suplocsrlemb  7768  axprecex  7842  axpre-ltwlin  7845  axpre-lttrn  7846  axpre-apti  7847  axpre-mulgt0  7849  axpre-mulext  7850  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  axsuploc  7992  ltleletr  8001  ltordlem  8401  squeeze0  8820  sup3exmid  8873  nnsub  8917  fzind  9327  uzind4s  9549  uzind4s2  9550  indstr  9552  supinfneg  9554  infsupneg  9555  frec2uzuzd  10358  frec2uzltd  10359  uzsinds  10398  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  seq3id2  10465  expcl2lemap  10488  nn0ltexp2  10644  facdiv  10672  facwordi  10674  zfz1isolem1  10775  zfz1iso  10776  seq3coll  10777  caucvgre  10945  fimaxre2  11190  climcn1  11271  climcn2  11272  subcn2  11274  summodclem2a  11344  fsumsplitf  11371  fsum2d  11398  modfsummod  11421  fsumabs  11428  telfsumo  11429  fsumiun  11440  prodfdivap  11510  fprod2d  11586  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  ndvdssub  11889  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemzz  11957  bezoutlemsup  11964  dfgcd2  11969  algcvg  12002  algcvga  12005  algfx  12006  lcmgcdlem  12031  lcmdvds  12033  coprmgcdb  12042  coprmdvds1  12045  coprmdvds2  12047  prmind2  12074  dvdsprime  12076  nprm  12077  dvdsprm  12091  exprmfct  12092  isprm5lem  12095  coprm  12098  isprm6  12101  prmfac1  12106  sqrt2irr  12116  pcqmul  12257  pcqcl  12260  pc2dvds  12283  pcz  12285  prmpwdvds  12307  ennnfonelemim  12379  exmidunben  12381  infpn2  12411  uniopn  12793  fiinopn  12796  epttop  12884  cnpval  12992  iscnp  12993  icnpimaex  13005  lmcvg  13011  cnptoprest  13033  cnptoprest2  13034  lmss  13040  lmff  13043  txcnp  13065  txlm  13073  cnmpt12  13081  cnmpt22  13088  blssps  13221  blss  13222  metss  13288  comet  13293  metcnp3  13305  metcnp2  13307  txmetcnp  13312  divcnap  13349  elcncf2  13355  cncfi  13359  mulc1cncf  13370  cncfmet  13373  mulcncflem  13384  mulcncf  13385  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeulemeu  13394  suplociccreex  13396  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemeu  13403  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  limccl  13422  ellimc3apf  13423  limccnpcntop  13438  limccnp2lem  13439  limccoap  13441  dvcoapbr  13465  lgsdir2lem4  13726  2sqlem6  13750  2sqlem8  13753  2sqlem10  13755  cbvrald  13823  bj-bdfindes  13984  bj-omtrans  13991  bj-inf2vnlem1  14005  bj-inf2vnlem2  14006  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  bj-findes  14016  strcoll2  14018  sscoll2  14023  exmid1stab  14033  subctctexmid  14034  pw1nct  14036  exmidsbthrlem  14054  sbthom  14058  apdiff  14080  ismkvnnlem  14084  nconstwlpolem  14096  neapmkv  14099