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  839  nfbidf  1587  drnf1  1781  drnf2  1782  equveli  1807  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  mobidh  2113  mobid  2114  axext3  2214  cbvralfw  2756  cbvralf  2758  cbvralvw  2771  cbvraldva2  2774  gencbval  2852  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  rspc2gv  2922  ceqex  2933  ralab2  2970  mob2  2986  mob  2988  morex  2990  reu7  3001  reu8  3002  nelrdva  3013  cdeqim  3024  sbcimg  3073  csbhypf  3166  cbvralcsf  3190  dfss2f  3218  sbcssg  3603  sneqrg  3845  elintab  3939  intss1  3943  intmin  3948  dfiin2g  4003  disji2  4080  disjiun  4083  trel  4194  trss  4196  bnd2  4263  zfpow  4265  exmidexmid  4286  exmidsssnc  4293  exmidundifim  4297  exmid1stab  4298  rext  4307  opth  4329  copsexg  4336  poeq1  4396  pocl  4400  swopolem  4402  swopo  4403  soeq1  4412  sowlin  4417  frforeq2  4442  frforeq3  4444  frirrg  4447  frind  4449  weeq1  4453  ordelord  4478  reusv3i  4556  ordtriexmid  4619  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  regexmid  4633  reg2exmid  4634  elirr  4639  en2lp  4652  ordsoexmid  4660  onintexmid  4671  reg3exmid  4678  tfis  4681  tfisi  4685  peano2  4693  findes  4701  nnregexmid  4719  omsinds  4720  vtoclr  4774  poinxp  4795  soinxp  4796  posng  4798  ssrel  4814  ssrel2  4816  ssrelrel  4826  relop  4880  issref  5119  iotaexab  5305  iota5  5308  dffun4f  5342  sbcfung  5350  funopg  5360  brprcneu  5632  funfveu  5652  tz6.12f  5668  funbrfv  5682  ssimaexg  5708  fvmptss2  5721  fvmptssdm  5731  fvmptf  5739  fvelrn  5778  f1veqaeq  5910  dff13f  5911  isopolem  5963  isosolem  5965  riota5f  5998  imbrov2fvoveq  6043  oprabid  6050  ovmpos  6145  ov2gf  6146  ovi3  6159  caovcan  6187  caovordig  6188  caofrss  6267  caoftrn  6268  dfoprab4f  6356  f1o2ndf1  6393  poxp  6397  smoel  6466  tfrlem1  6474  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  nnsucelsuc  6659  nnsucsssuc  6660  nnmordi  6684  nnaordex  6696  qsel  6781  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem2  6807  ixpsnf1o  6905  fundmeng  6982  modom  6994  phplem3g  7042  nneneq  7043  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard  7077  findcard2  7078  findcard2s  7079  findcard2d  7080  findcard2sd  7081  diffifi  7083  ac6sfi  7087  fiintim  7123  fisseneq  7127  fidcenumlemrk  7153  fidcenumlemr  7154  isbth  7166  supeq3  7189  supeq123d  7190  supmoti  7192  suplubti  7199  supisolem  7207  cnvinfex  7217  eqinfti  7219  infvalti  7221  ordiso2  7234  nninfninc  7322  nnnninfeq2  7328  isomni  7335  finomni  7339  exmidomni  7341  ctssexmid  7349  ismkv  7352  ismkvnex  7354  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  iswomni  7364  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  tapeq1  7471  exmidapne  7479  ccfunen  7483  ltsonq  7618  ltexnqq  7628  prcdnql  7704  prcunqu  7705  prloc  7711  prdisj  7712  genprndl  7741  genprndu  7742  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgprprlemcbv  7907  caucvgprprlemval  7908  suplocexprlemloc  7941  lttrsr  7982  ltsosr  7984  recexgt0sr  7993  mulgt0sr  7998  aptisr  7999  mulextsr1  8001  srpospr  8003  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  map2psrprg  8025  suplocsrlemb  8026  axprecex  8100  axpre-ltwlin  8103  axpre-lttrn  8104  axpre-apti  8105  axpre-mulgt0  8107  axpre-mulext  8108  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  axsuploc  8252  ltleletr  8261  ltordlem  8662  squeeze0  9084  sup3exmid  9137  nnsub  9182  fzind  9595  uzind4s  9824  uzind4s2  9825  indstr  9827  supinfneg  9829  infsupneg  9830  frec2uzuzd  10665  frec2uzltd  10666  uzsinds  10707  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seqf1oglem2  10783  seqf1og  10784  seq3id2  10789  seqhomog  10793  expcl2lemap  10814  nn0ltexp2  10972  facdiv  11001  facwordi  11003  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccat3blem  11324  reuccatpfxs1lem  11331  caucvgre  11559  fimaxre2  11805  climcn1  11886  climcn2  11887  subcn2  11889  summodclem2a  11960  fsumsplitf  11987  fsum2d  12014  modfsummod  12037  fsumabs  12044  telfsumo  12045  fsumiun  12056  prodfdivap  12126  fprod2d  12202  fproddivapf  12210  fprodsplitf  12211  fprodsplit1f  12213  ndvdssub  12509  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemzz  12591  bezoutlemsup  12598  dfgcd2  12603  algcvg  12638  algcvga  12641  algfx  12642  lcmgcdlem  12667  lcmdvds  12669  coprmgcdb  12678  coprmdvds1  12681  coprmdvds2  12683  prmind2  12710  dvdsprime  12712  nprm  12713  dvdsprm  12727  exprmfct  12728  isprm5lem  12731  coprm  12734  isprm6  12737  prmfac1  12742  sqrt2irr  12752  pcqmul  12894  pcqcl  12897  pc2dvds  12921  pcz  12923  prmpwdvds  12946  ennnfonelemim  13063  exmidunben  13065  infpn2  13095  setscomd  13141  mhmlem  13719  isnsg2  13808  ghmf1  13878  islring  14225  lringuplu  14229  rrgval  14295  rrgeq0i  14297  isdomn  14302  domneq0  14305  opprdomnbg  14307  znidom  14690  znrrg  14693  mplvalcoe  14723  mplsubgfilemcl  14732  uniopn  14744  fiinopn  14747  epttop  14833  cnpval  14941  iscnp  14942  icnpimaex  14954  lmcvg  14960  cnptoprest  14982  cnptoprest2  14983  lmss  14989  lmff  14992  txcnp  15014  txlm  15022  cnmpt12  15030  cnmpt22  15037  blssps  15170  blss  15171  metss  15237  comet  15242  metcnp3  15254  metcnp2  15256  txmetcnp  15261  divcnap  15308  mpomulcn  15309  elcncf2  15317  cncfi  15321  mulc1cncf  15332  cncfmet  15335  mulcncflem  15350  mulcncf  15351  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeulemeu  15365  suplociccreex  15367  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemeu  15374  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthreinc  15388  limccl  15402  ellimc3apf  15403  limccnpcntop  15418  limccnp2lem  15419  limccoap  15421  dvcoapbr  15450  dvmptfsum  15468  mpodvdsmulf1o  15733  perfectlem2  15743  lgsdir2lem4  15779  gausslemma2dlem0i  15805  lgseisenlem2  15819  lgsquad2lem2  15830  2sqlem6  15868  2sqlem8  15871  2sqlem10  15873  gropd  15917  grstructd2dom  15918  upgredg2vtx  16018  upgredgpr  16019  eupth2fi  16349  cbvrald  16435  bj-bdfindes  16595  bj-omtrans  16602  bj-inf2vnlem1  16616  bj-inf2vnlem2  16617  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619  bj-findes  16627  strcoll2  16629  sscoll2  16634  subctctexmid  16652  pw1nct  16655  exmidsbthrlem  16677  sbthom  16681  apdiff  16703  ismkvnnlem  16708  nconstwlpolem  16721  neapmkv  16724  neap0mkv  16725  ltlenmkv  16726