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  833  nfbidf  1553  drnf1  1747  drnf2  1748  equveli  1773  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  mobidh  2079  mobid  2080  axext3  2179  cbvralfw  2719  cbvralf  2721  cbvralvw  2733  cbvraldva2  2736  gencbval  2812  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  rspc2gv  2880  ceqex  2891  ralab2  2928  mob2  2944  mob  2946  morex  2948  reu7  2959  reu8  2960  nelrdva  2971  cdeqim  2982  sbcimg  3031  csbhypf  3123  cbvralcsf  3147  dfss2f  3174  sbcssg  3559  sneqrg  3792  elintab  3885  intss1  3889  intmin  3894  dfiin2g  3949  disji2  4026  disjiun  4028  trel  4138  trss  4140  bnd2  4206  zfpow  4208  exmidexmid  4229  exmidsssnc  4236  exmidundifim  4240  exmid1stab  4241  rext  4248  opth  4270  copsexg  4277  poeq1  4334  pocl  4338  swopolem  4340  swopo  4341  soeq1  4350  sowlin  4355  frforeq2  4380  frforeq3  4382  frirrg  4385  frind  4387  weeq1  4391  ordelord  4416  reusv3i  4494  ordtriexmid  4557  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmid  4566  ordsucunielexmid  4567  regexmidlem1  4569  regexmid  4571  reg2exmid  4572  elirr  4577  en2lp  4590  ordsoexmid  4598  onintexmid  4609  reg3exmid  4616  tfis  4619  tfisi  4623  peano2  4631  findes  4639  nnregexmid  4657  omsinds  4658  vtoclr  4711  poinxp  4732  soinxp  4733  posng  4735  ssrel  4751  ssrel2  4753  ssrelrel  4763  relop  4816  issref  5052  iotaexab  5237  iota5  5240  dffun4f  5274  sbcfung  5282  funopg  5292  brprcneu  5551  funfveu  5571  tz6.12f  5587  funbrfv  5599  ssimaexg  5623  fvmptss2  5636  fvmptssdm  5646  fvmptf  5654  fvelrn  5693  f1veqaeq  5816  dff13f  5817  isopolem  5869  isosolem  5871  riota5f  5902  imbrov2fvoveq  5947  oprabid  5954  ovmpos  6046  ov2gf  6047  ovi3  6060  caovcan  6088  caovordig  6089  caofrss  6162  caoftrn  6163  dfoprab4f  6251  f1o2ndf1  6286  poxp  6290  smoel  6358  tfrlem1  6366  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  nnsucelsuc  6549  nnsucsssuc  6550  nnmordi  6574  nnaordex  6586  qsel  6671  eroveu  6685  ecopovtrn  6691  ecopovtrng  6694  th3qlem2  6697  ixpsnf1o  6795  fundmeng  6866  phplem3g  6917  nneneq  6918  ssfiexmid  6937  domfiexmid  6939  findcard  6949  findcard2  6950  findcard2s  6951  findcard2d  6952  findcard2sd  6953  diffifi  6955  ac6sfi  6959  fiintim  6992  fisseneq  6995  fidcenumlemrk  7020  fidcenumlemr  7021  isbth  7033  supeq3  7056  supeq123d  7057  supmoti  7059  suplubti  7066  supisolem  7074  cnvinfex  7084  eqinfti  7086  infvalti  7088  ordiso2  7101  nninfninc  7189  nnnninfeq2  7195  isomni  7202  finomni  7206  exmidomni  7208  ctssexmid  7216  ismkv  7219  ismkvnex  7221  mkvprop  7224  fodjumkvlemres  7225  enmkvlem  7227  iswomni  7231  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  tapeq1  7319  exmidapne  7327  ccfunen  7331  ltsonq  7465  ltexnqq  7475  prcdnql  7551  prcunqu  7552  prloc  7558  prdisj  7559  genprndl  7588  genprndu  7589  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemcl  7743  caucvgprprlemcbv  7754  caucvgprprlemval  7755  suplocexprlemloc  7788  lttrsr  7829  ltsosr  7831  recexgt0sr  7840  mulgt0sr  7845  aptisr  7846  mulextsr1  7848  srpospr  7850  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  caucvgsr  7869  map2psrprg  7872  suplocsrlemb  7873  axprecex  7947  axpre-ltwlin  7950  axpre-lttrn  7951  axpre-apti  7952  axpre-mulgt0  7954  axpre-mulext  7955  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  axsuploc  8099  ltleletr  8108  ltordlem  8509  squeeze0  8931  sup3exmid  8984  nnsub  9029  fzind  9441  uzind4s  9664  uzind4s2  9665  indstr  9667  supinfneg  9669  infsupneg  9670  frec2uzuzd  10494  frec2uzltd  10495  uzsinds  10536  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  seqf1oglem2  10612  seqf1og  10613  seq3id2  10618  seqhomog  10622  expcl2lemap  10643  nn0ltexp2  10801  facdiv  10830  facwordi  10832  zfz1isolem1  10932  zfz1iso  10933  seq3coll  10934  caucvgre  11146  fimaxre2  11392  climcn1  11473  climcn2  11474  subcn2  11476  summodclem2a  11546  fsumsplitf  11573  fsum2d  11600  modfsummod  11623  fsumabs  11630  telfsumo  11631  fsumiun  11642  prodfdivap  11712  fprod2d  11788  fproddivapf  11796  fprodsplitf  11797  fprodsplit1f  11799  ndvdssub  12095  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemzz  12169  bezoutlemsup  12176  dfgcd2  12181  algcvg  12216  algcvga  12219  algfx  12220  lcmgcdlem  12245  lcmdvds  12247  coprmgcdb  12256  coprmdvds1  12259  coprmdvds2  12261  prmind2  12288  dvdsprime  12290  nprm  12291  dvdsprm  12305  exprmfct  12306  isprm5lem  12309  coprm  12312  isprm6  12315  prmfac1  12320  sqrt2irr  12330  pcqmul  12472  pcqcl  12475  pc2dvds  12499  pcz  12501  prmpwdvds  12524  ennnfonelemim  12641  exmidunben  12643  infpn2  12673  setscomd  12719  mhmlem  13244  isnsg2  13333  ghmf1  13403  islring  13748  lringuplu  13752  rrgval  13818  rrgeq0i  13820  isdomn  13825  domneq0  13828  opprdomnbg  13830  znidom  14213  znrrg  14216  uniopn  14237  fiinopn  14240  epttop  14326  cnpval  14434  iscnp  14435  icnpimaex  14447  lmcvg  14453  cnptoprest  14475  cnptoprest2  14476  lmss  14482  lmff  14485  txcnp  14507  txlm  14515  cnmpt12  14523  cnmpt22  14530  blssps  14663  blss  14664  metss  14730  comet  14735  metcnp3  14747  metcnp2  14749  txmetcnp  14754  divcnap  14801  mpomulcn  14802  elcncf2  14810  cncfi  14814  mulc1cncf  14825  cncfmet  14828  mulcncflem  14843  mulcncf  14844  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeulemeu  14858  suplociccreex  14860  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemeu  14867  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthreinc  14881  limccl  14895  ellimc3apf  14896  limccnpcntop  14911  limccnp2lem  14912  limccoap  14914  dvcoapbr  14943  dvmptfsum  14961  mpodvdsmulf1o  15226  perfectlem2  15236  lgsdir2lem4  15272  gausslemma2dlem0i  15298  lgseisenlem2  15312  lgsquad2lem2  15323  2sqlem6  15361  2sqlem8  15364  2sqlem10  15366  cbvrald  15434  bj-bdfindes  15595  bj-omtrans  15602  bj-inf2vnlem1  15616  bj-inf2vnlem2  15617  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  bj-findes  15627  strcoll2  15629  sscoll2  15634  subctctexmid  15645  pw1nct  15647  exmidsbthrlem  15666  sbthom  15670  apdiff  15692  ismkvnnlem  15696  nconstwlpolem  15709  neapmkv  15712  neap0mkv  15713  ltlenmkv  15714