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  834  nfbidf  1563  drnf1  1757  drnf2  1758  equveli  1783  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  mobidh  2089  mobid  2090  axext3  2190  cbvralfw  2731  cbvralf  2733  cbvralvw  2746  cbvraldva2  2749  gencbval  2826  vtoclgaf  2843  vtocl2gaf  2845  vtocl3gaf  2847  rspct  2877  rspc  2878  rspc2gv  2896  ceqex  2907  ralab2  2944  mob2  2960  mob  2962  morex  2964  reu7  2975  reu8  2976  nelrdva  2987  cdeqim  2998  sbcimg  3047  csbhypf  3140  cbvralcsf  3164  dfss2f  3192  sbcssg  3577  sneqrg  3816  elintab  3910  intss1  3914  intmin  3919  dfiin2g  3974  disji2  4051  disjiun  4054  trel  4165  trss  4167  bnd2  4233  zfpow  4235  exmidexmid  4256  exmidsssnc  4263  exmidundifim  4267  exmid1stab  4268  rext  4277  opth  4299  copsexg  4306  poeq1  4364  pocl  4368  swopolem  4370  swopo  4371  soeq1  4380  sowlin  4385  frforeq2  4410  frforeq3  4412  frirrg  4415  frind  4417  weeq1  4421  ordelord  4446  reusv3i  4524  ordtriexmid  4587  ontr2exmid  4591  onsucsssucexmid  4593  onsucelsucexmid  4596  ordsucunielexmid  4597  regexmidlem1  4599  regexmid  4601  reg2exmid  4602  elirr  4607  en2lp  4620  ordsoexmid  4628  onintexmid  4639  reg3exmid  4646  tfis  4649  tfisi  4653  peano2  4661  findes  4669  nnregexmid  4687  omsinds  4688  vtoclr  4741  poinxp  4762  soinxp  4763  posng  4765  ssrel  4781  ssrel2  4783  ssrelrel  4793  relop  4846  issref  5084  iotaexab  5269  iota5  5272  dffun4f  5306  sbcfung  5314  funopg  5324  brprcneu  5592  funfveu  5612  tz6.12f  5628  funbrfv  5640  ssimaexg  5664  fvmptss2  5677  fvmptssdm  5687  fvmptf  5695  fvelrn  5734  f1veqaeq  5861  dff13f  5862  isopolem  5914  isosolem  5916  riota5f  5947  imbrov2fvoveq  5992  oprabid  5999  ovmpos  6092  ov2gf  6093  ovi3  6106  caovcan  6134  caovordig  6135  caofrss  6213  caoftrn  6214  dfoprab4f  6302  f1o2ndf1  6337  poxp  6341  smoel  6409  tfrlem1  6417  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  nnsucelsuc  6600  nnsucsssuc  6601  nnmordi  6625  nnaordex  6637  qsel  6722  eroveu  6736  ecopovtrn  6742  ecopovtrng  6745  th3qlem2  6748  ixpsnf1o  6846  fundmeng  6923  phplem3g  6978  nneneq  6979  ssfiexmid  6999  domfiexmid  7001  findcard  7011  findcard2  7012  findcard2s  7013  findcard2d  7014  findcard2sd  7015  diffifi  7017  ac6sfi  7021  fiintim  7054  fisseneq  7057  fidcenumlemrk  7082  fidcenumlemr  7083  isbth  7095  supeq3  7118  supeq123d  7119  supmoti  7121  suplubti  7128  supisolem  7136  cnvinfex  7146  eqinfti  7148  infvalti  7150  ordiso2  7163  nninfninc  7251  nnnninfeq2  7257  isomni  7264  finomni  7268  exmidomni  7270  ctssexmid  7278  ismkv  7281  ismkvnex  7283  mkvprop  7286  fodjumkvlemres  7287  enmkvlem  7289  iswomni  7293  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  tapeq1  7399  exmidapne  7407  ccfunen  7411  ltsonq  7546  ltexnqq  7556  prcdnql  7632  prcunqu  7633  prloc  7639  prdisj  7640  genprndl  7669  genprndu  7670  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemcl  7824  caucvgprprlemcbv  7835  caucvgprprlemval  7836  suplocexprlemloc  7869  lttrsr  7910  ltsosr  7912  recexgt0sr  7921  mulgt0sr  7926  aptisr  7927  mulextsr1  7929  srpospr  7931  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  caucvgsr  7950  map2psrprg  7953  suplocsrlemb  7954  axprecex  8028  axpre-ltwlin  8031  axpre-lttrn  8032  axpre-apti  8033  axpre-mulgt0  8035  axpre-mulext  8036  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  axpre-suploc  8050  axsuploc  8180  ltleletr  8189  ltordlem  8590  squeeze0  9012  sup3exmid  9065  nnsub  9110  fzind  9523  uzind4s  9746  uzind4s2  9747  indstr  9749  supinfneg  9751  infsupneg  9752  frec2uzuzd  10584  frec2uzltd  10585  uzsinds  10626  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord  10667  seq3split  10670  seqsplitg  10671  seqf1oglem2  10702  seqf1og  10703  seq3id2  10708  seqhomog  10712  expcl2lemap  10733  nn0ltexp2  10891  facdiv  10920  facwordi  10922  zfz1isolem1  11022  zfz1iso  11023  seq3coll  11024  wrdind  11213  wrd2ind  11214  swrdccatin1  11216  swrdccat3blem  11230  reuccatpfxs1lem  11237  caucvgre  11407  fimaxre2  11653  climcn1  11734  climcn2  11735  subcn2  11737  summodclem2a  11807  fsumsplitf  11834  fsum2d  11861  modfsummod  11884  fsumabs  11891  telfsumo  11892  fsumiun  11903  prodfdivap  11973  fprod2d  12049  fproddivapf  12057  fprodsplitf  12058  fprodsplit1f  12060  ndvdssub  12356  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemzz  12438  bezoutlemsup  12445  dfgcd2  12450  algcvg  12485  algcvga  12488  algfx  12489  lcmgcdlem  12514  lcmdvds  12516  coprmgcdb  12525  coprmdvds1  12528  coprmdvds2  12530  prmind2  12557  dvdsprime  12559  nprm  12560  dvdsprm  12574  exprmfct  12575  isprm5lem  12578  coprm  12581  isprm6  12584  prmfac1  12589  sqrt2irr  12599  pcqmul  12741  pcqcl  12744  pc2dvds  12768  pcz  12770  prmpwdvds  12793  ennnfonelemim  12910  exmidunben  12912  infpn2  12942  setscomd  12988  mhmlem  13565  isnsg2  13654  ghmf1  13724  islring  14069  lringuplu  14073  rrgval  14139  rrgeq0i  14141  isdomn  14146  domneq0  14149  opprdomnbg  14151  znidom  14534  znrrg  14537  mplvalcoe  14567  mplsubgfilemcl  14576  uniopn  14588  fiinopn  14591  epttop  14677  cnpval  14785  iscnp  14786  icnpimaex  14798  lmcvg  14804  cnptoprest  14826  cnptoprest2  14827  lmss  14833  lmff  14836  txcnp  14858  txlm  14866  cnmpt12  14874  cnmpt22  14881  blssps  15014  blss  15015  metss  15081  comet  15086  metcnp3  15098  metcnp2  15100  txmetcnp  15105  divcnap  15152  mpomulcn  15153  elcncf2  15161  cncfi  15165  mulc1cncf  15176  cncfmet  15179  mulcncflem  15194  mulcncf  15195  dedekindeulemloc  15206  dedekindeulemlu  15208  dedekindeulemeu  15209  suplociccreex  15211  dedekindicclemloc  15215  dedekindicclemlu  15217  dedekindicclemeu  15218  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemloc  15228  ivthreinc  15232  limccl  15246  ellimc3apf  15247  limccnpcntop  15262  limccnp2lem  15263  limccoap  15265  dvcoapbr  15294  dvmptfsum  15312  mpodvdsmulf1o  15577  perfectlem2  15587  lgsdir2lem4  15623  gausslemma2dlem0i  15649  lgseisenlem2  15663  lgsquad2lem2  15674  2sqlem6  15712  2sqlem8  15715  2sqlem10  15717  gropd  15761  grstructd2dom  15762  upgredg2vtx  15852  upgredgpr  15853  cbvrald  15924  bj-bdfindes  16084  bj-omtrans  16091  bj-inf2vnlem1  16105  bj-inf2vnlem2  16106  bj-inf2vnlem3  16107  bj-inf2vnlem4  16108  bj-findes  16116  strcoll2  16118  sscoll2  16123  subctctexmid  16139  pw1nct  16142  exmidsbthrlem  16163  sbthom  16167  apdiff  16189  ismkvnnlem  16193  nconstwlpolem  16206  neapmkv  16209  neap0mkv  16210  ltlenmkv  16211