Theorem imbi12d 234

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 231	. 2 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	imbi2d 230	. 2 |- ( ph -> ( ( ch -> th ) <-> ( ch -> ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  832  nfbidf  1537  drnf1  1731  drnf2  1732  equveli  1757  ax11v2  1818  ax11v  1825  ax11ev  1826  equs5or  1828  mobidh  2058  mobid  2059  axext3  2158  cbvralfw  2692  cbvralf  2694  cbvralvw  2705  cbvraldva2  2708  gencbval  2783  vtoclgaf  2800  vtocl2gaf  2802  vtocl3gaf  2804  rspct  2832  rspc  2833  rspc2gv  2851  ceqex  2862  ralab2  2899  mob2  2915  mob  2917  morex  2919  reu7  2930  reu8  2931  nelrdva  2942  cdeqim  2953  sbcimg  3002  csbhypf  3093  cbvralcsf  3117  dfss2f  3144  sbcssg  3530  sneqrg  3758  elintab  3851  intss1  3855  intmin  3860  dfiin2g  3915  disji2  3991  disjiun  3993  trel  4103  trss  4105  bnd2  4168  zfpow  4170  exmidexmid  4191  exmidsssnc  4198  exmidundifim  4202  rext  4209  opth  4231  copsexg  4238  poeq1  4293  pocl  4297  swopolem  4299  swopo  4300  soeq1  4309  sowlin  4314  frforeq2  4339  frforeq3  4341  frirrg  4344  frind  4346  weeq1  4350  ordelord  4375  reusv3i  4453  ordtriexmid  4514  ontr2exmid  4518  onsucsssucexmid  4520  onsucelsucexmid  4523  ordsucunielexmid  4524  regexmidlem1  4526  regexmid  4528  reg2exmid  4529  elirr  4534  en2lp  4547  ordsoexmid  4555  onintexmid  4566  reg3exmid  4573  tfis  4576  tfisi  4580  peano2  4588  findes  4596  nnregexmid  4614  omsinds  4615  vtoclr  4668  poinxp  4689  soinxp  4690  posng  4692  ssrel  4708  ssrel2  4710  ssrelrel  4720  relop  4770  issref  5003  iota5  5190  dffun4f  5224  sbcfung  5232  funopg  5242  brprcneu  5500  funfveu  5520  tz6.12f  5536  funbrfv  5546  ssimaexg  5570  fvmptss2  5583  fvmptssdm  5592  fvmptf  5600  fvelrn  5639  f1veqaeq  5760  dff13f  5761  isopolem  5813  isosolem  5815  riota5f  5845  imbrov2fvoveq  5890  oprabid  5897  ovmpos  5988  ov2gf  5989  ovi3  6001  caovcan  6029  caovordig  6030  caofrss  6097  caoftrn  6098  dfoprab4f  6184  f1o2ndf1  6219  poxp  6223  smoel  6291  tfrlem1  6299  tfr1onlemsucfn  6331  tfr1onlemsucaccv  6332  tfr1onlembxssdm  6334  tfr1onlembfn  6335  tfr1onlemaccex  6339  tfr1onlemres  6340  tfrcllemsucfn  6344  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllembfn  6348  tfrcllemaccex  6352  tfrcllemres  6353  tfrcl  6355  nnsucelsuc  6482  nnsucsssuc  6483  nnmordi  6507  nnaordex  6519  qsel  6602  eroveu  6616  ecopovtrn  6622  ecopovtrng  6625  th3qlem2  6628  ixpsnf1o  6726  fundmeng  6797  phplem3g  6846  nneneq  6847  ssfiexmid  6866  domfiexmid  6868  findcard  6878  findcard2  6879  findcard2s  6880  findcard2d  6881  findcard2sd  6882  diffifi  6884  ac6sfi  6888  fiintim  6918  fisseneq  6921  fidcenumlemrk  6943  fidcenumlemr  6944  isbth  6956  supeq3  6979  supeq123d  6980  supmoti  6982  suplubti  6989  supisolem  6997  cnvinfex  7007  eqinfti  7009  infvalti  7011  ordiso2  7024  nnnninfeq2  7117  isomni  7124  finomni  7128  exmidomni  7130  ctssexmid  7138  ismkv  7141  ismkvnex  7143  mkvprop  7146  fodjumkvlemres  7147  enmkvlem  7149  iswomni  7153  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  ccfunen  7238  ltsonq  7372  ltexnqq  7382  prcdnql  7458  prcunqu  7459  prloc  7465  prdisj  7466  genprndl  7495  genprndu  7496  caucvgprlemnkj  7640  caucvgprlemnbj  7641  caucvgprlemcl  7650  caucvgprprlemcbv  7661  caucvgprprlemval  7662  suplocexprlemloc  7695  lttrsr  7736  ltsosr  7738  recexgt0sr  7747  mulgt0sr  7752  aptisr  7753  mulextsr1  7755  srpospr  7757  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  caucvgsr  7776  map2psrprg  7779  suplocsrlemb  7780  axprecex  7854  axpre-ltwlin  7857  axpre-lttrn  7858  axpre-apti  7859  axpre-mulgt0  7861  axpre-mulext  7862  axcaucvglemcau  7872  axcaucvglemres  7873  axpre-suploclemres  7875  axpre-suploc  7876  axsuploc  8004  ltleletr  8013  ltordlem  8413  squeeze0  8834  sup3exmid  8887  nnsub  8931  fzind  9341  uzind4s  9563  uzind4s2  9564  indstr  9566  supinfneg  9568  infsupneg  9569  frec2uzuzd  10372  frec2uzltd  10373  uzsinds  10412  seq3fveq2  10439  seq3shft2  10443  monoord  10446  seq3split  10449  seq3id2  10479  expcl2lemap  10502  nn0ltexp2  10658  facdiv  10686  facwordi  10688  zfz1isolem1  10788  zfz1iso  10789  seq3coll  10790  caucvgre  10958  fimaxre2  11203  climcn1  11284  climcn2  11285  subcn2  11287  summodclem2a  11357  fsumsplitf  11384  fsum2d  11411  modfsummod  11434  fsumabs  11441  telfsumo  11442  fsumiun  11453  prodfdivap  11523  fprod2d  11599  fproddivapf  11607  fprodsplitf  11608  fprodsplit1f  11610  ndvdssub  11902  bezoutlemmain  11966  bezoutlemex  11969  bezoutlemzz  11970  bezoutlemsup  11977  dfgcd2  11982  algcvg  12015  algcvga  12018  algfx  12019  lcmgcdlem  12044  lcmdvds  12046  coprmgcdb  12055  coprmdvds1  12058  coprmdvds2  12060  prmind2  12087  dvdsprime  12089  nprm  12090  dvdsprm  12104  exprmfct  12105  isprm5lem  12108  coprm  12111  isprm6  12114  prmfac1  12119  sqrt2irr  12129  pcqmul  12270  pcqcl  12273  pc2dvds  12296  pcz  12298  prmpwdvds  12320  ennnfonelemim  12392  exmidunben  12394  infpn2  12424  mhmlem  12839  uniopn  13070  fiinopn  13073  epttop  13161  cnpval  13269  iscnp  13270  icnpimaex  13282  lmcvg  13288  cnptoprest  13310  cnptoprest2  13311  lmss  13317  lmff  13320  txcnp  13342  txlm  13350  cnmpt12  13358  cnmpt22  13365  blssps  13498  blss  13499  metss  13565  comet  13570  metcnp3  13582  metcnp2  13584  txmetcnp  13589  divcnap  13626  elcncf2  13632  cncfi  13636  mulc1cncf  13647  cncfmet  13650  mulcncflem  13661  mulcncf  13662  dedekindeulemloc  13668  dedekindeulemlu  13670  dedekindeulemeu  13671  suplociccreex  13673  dedekindicclemloc  13677  dedekindicclemlu  13679  dedekindicclemeu  13680  ivthinclemlopn  13685  ivthinclemlr  13686  ivthinclemuopn  13687  ivthinclemur  13688  ivthinclemloc  13690  limccl  13699  ellimc3apf  13700  limccnpcntop  13715  limccnp2lem  13716  limccoap  13718  dvcoapbr  13742  lgsdir2lem4  14003  2sqlem6  14027  2sqlem8  14030  2sqlem10  14032  cbvrald  14100  bj-bdfindes  14261  bj-omtrans  14268  bj-inf2vnlem1  14282  bj-inf2vnlem2  14283  bj-inf2vnlem3  14284  bj-inf2vnlem4  14285  bj-findes  14293  strcoll2  14295  sscoll2  14300  exmid1stab  14310  subctctexmid  14311  pw1nct  14313  exmidsbthrlem  14331  sbthom  14335  apdiff  14357  ismkvnnlem  14361  nconstwlpolem  14373  neapmkv  14376