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  837  nfbidf  1585  drnf1  1779  drnf2  1780  equveli  1805  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  mobidh  2111  mobid  2112  axext3  2212  cbvralfw  2754  cbvralf  2756  cbvralvw  2769  cbvraldva2  2772  gencbval  2849  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspc2gv  2919  ceqex  2930  ralab2  2967  mob2  2983  mob  2985  morex  2987  reu7  2998  reu8  2999  nelrdva  3010  cdeqim  3021  sbcimg  3070  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  sbcssg  3600  sneqrg  3839  elintab  3933  intss1  3937  intmin  3942  dfiin2g  3997  disji2  4074  disjiun  4077  trel  4188  trss  4190  bnd2  4256  zfpow  4258  exmidexmid  4279  exmidsssnc  4286  exmidundifim  4290  exmid1stab  4291  rext  4300  opth  4322  copsexg  4329  poeq1  4389  pocl  4393  swopolem  4395  swopo  4396  soeq1  4405  sowlin  4410  frforeq2  4435  frforeq3  4437  frirrg  4440  frind  4442  weeq1  4446  ordelord  4471  reusv3i  4549  ordtriexmid  4612  ontr2exmid  4616  onsucsssucexmid  4618  onsucelsucexmid  4621  ordsucunielexmid  4622  regexmidlem1  4624  regexmid  4626  reg2exmid  4627  elirr  4632  en2lp  4645  ordsoexmid  4653  onintexmid  4664  reg3exmid  4671  tfis  4674  tfisi  4678  peano2  4686  findes  4694  nnregexmid  4712  omsinds  4713  vtoclr  4766  poinxp  4787  soinxp  4788  posng  4790  ssrel  4806  ssrel2  4808  ssrelrel  4818  relop  4871  issref  5110  iotaexab  5296  iota5  5299  dffun4f  5333  sbcfung  5341  funopg  5351  brprcneu  5619  funfveu  5639  tz6.12f  5655  funbrfv  5669  ssimaexg  5695  fvmptss2  5708  fvmptssdm  5718  fvmptf  5726  fvelrn  5765  f1veqaeq  5892  dff13f  5893  isopolem  5945  isosolem  5947  riota5f  5980  imbrov2fvoveq  6025  oprabid  6032  ovmpos  6127  ov2gf  6128  ovi3  6141  caovcan  6169  caovordig  6170  caofrss  6248  caoftrn  6249  dfoprab4f  6337  f1o2ndf1  6372  poxp  6376  smoel  6444  tfrlem1  6452  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemaccex  6505  tfrcllemres  6506  tfrcl  6508  nnsucelsuc  6635  nnsucsssuc  6636  nnmordi  6660  nnaordex  6672  qsel  6757  eroveu  6771  ecopovtrn  6777  ecopovtrng  6780  th3qlem2  6783  ixpsnf1o  6881  fundmeng  6958  phplem3g  7013  nneneq  7014  ssfiexmid  7034  domfiexmid  7036  findcard  7046  findcard2  7047  findcard2s  7048  findcard2d  7049  findcard2sd  7050  diffifi  7052  ac6sfi  7056  fiintim  7089  fisseneq  7092  fidcenumlemrk  7117  fidcenumlemr  7118  isbth  7130  supeq3  7153  supeq123d  7154  supmoti  7156  suplubti  7163  supisolem  7171  cnvinfex  7181  eqinfti  7183  infvalti  7185  ordiso2  7198  nninfninc  7286  nnnninfeq2  7292  isomni  7299  finomni  7303  exmidomni  7305  ctssexmid  7313  ismkv  7316  ismkvnex  7318  mkvprop  7321  fodjumkvlemres  7322  enmkvlem  7324  iswomni  7328  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  tapeq1  7434  exmidapne  7442  ccfunen  7446  ltsonq  7581  ltexnqq  7591  prcdnql  7667  prcunqu  7668  prloc  7674  prdisj  7675  genprndl  7704  genprndu  7705  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemcl  7859  caucvgprprlemcbv  7870  caucvgprprlemval  7871  suplocexprlemloc  7904  lttrsr  7945  ltsosr  7947  recexgt0sr  7956  mulgt0sr  7961  aptisr  7962  mulextsr1  7964  srpospr  7966  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  caucvgsr  7985  map2psrprg  7988  suplocsrlemb  7989  axprecex  8063  axpre-ltwlin  8066  axpre-lttrn  8067  axpre-apti  8068  axpre-mulgt0  8070  axpre-mulext  8071  axcaucvglemcau  8081  axcaucvglemres  8082  axpre-suploclemres  8084  axpre-suploc  8085  axsuploc  8215  ltleletr  8224  ltordlem  8625  squeeze0  9047  sup3exmid  9100  nnsub  9145  fzind  9558  uzind4s  9781  uzind4s2  9782  indstr  9784  supinfneg  9786  infsupneg  9787  frec2uzuzd  10619  frec2uzltd  10620  uzsinds  10661  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord  10702  seq3split  10705  seqsplitg  10706  seqf1oglem2  10737  seqf1og  10738  seq3id2  10743  seqhomog  10747  expcl2lemap  10768  nn0ltexp2  10926  facdiv  10955  facwordi  10957  zfz1isolem1  11057  zfz1iso  11058  seq3coll  11059  wrdind  11249  wrd2ind  11250  swrdccatin1  11252  swrdccat3blem  11266  reuccatpfxs1lem  11273  caucvgre  11487  fimaxre2  11733  climcn1  11814  climcn2  11815  subcn2  11817  summodclem2a  11887  fsumsplitf  11914  fsum2d  11941  modfsummod  11964  fsumabs  11971  telfsumo  11972  fsumiun  11983  prodfdivap  12053  fprod2d  12129  fproddivapf  12137  fprodsplitf  12138  fprodsplit1f  12140  ndvdssub  12436  bezoutlemmain  12514  bezoutlemex  12517  bezoutlemzz  12518  bezoutlemsup  12525  dfgcd2  12530  algcvg  12565  algcvga  12568  algfx  12569  lcmgcdlem  12594  lcmdvds  12596  coprmgcdb  12605  coprmdvds1  12608  coprmdvds2  12610  prmind2  12637  dvdsprime  12639  nprm  12640  dvdsprm  12654  exprmfct  12655  isprm5lem  12658  coprm  12661  isprm6  12664  prmfac1  12669  sqrt2irr  12679  pcqmul  12821  pcqcl  12824  pc2dvds  12848  pcz  12850  prmpwdvds  12873  ennnfonelemim  12990  exmidunben  12992  infpn2  13022  setscomd  13068  mhmlem  13646  isnsg2  13735  ghmf1  13805  islring  14150  lringuplu  14154  rrgval  14220  rrgeq0i  14222  isdomn  14227  domneq0  14230  opprdomnbg  14232  znidom  14615  znrrg  14618  mplvalcoe  14648  mplsubgfilemcl  14657  uniopn  14669  fiinopn  14672  epttop  14758  cnpval  14866  iscnp  14867  icnpimaex  14879  lmcvg  14885  cnptoprest  14907  cnptoprest2  14908  lmss  14914  lmff  14917  txcnp  14939  txlm  14947  cnmpt12  14955  cnmpt22  14962  blssps  15095  blss  15096  metss  15162  comet  15167  metcnp3  15179  metcnp2  15181  txmetcnp  15186  divcnap  15233  mpomulcn  15234  elcncf2  15242  cncfi  15246  mulc1cncf  15257  cncfmet  15260  mulcncflem  15275  mulcncf  15276  dedekindeulemloc  15287  dedekindeulemlu  15289  dedekindeulemeu  15290  suplociccreex  15292  dedekindicclemloc  15296  dedekindicclemlu  15298  dedekindicclemeu  15299  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemloc  15309  ivthreinc  15313  limccl  15327  ellimc3apf  15328  limccnpcntop  15343  limccnp2lem  15344  limccoap  15346  dvcoapbr  15375  dvmptfsum  15393  mpodvdsmulf1o  15658  perfectlem2  15668  lgsdir2lem4  15704  gausslemma2dlem0i  15730  lgseisenlem2  15744  lgsquad2lem2  15755  2sqlem6  15793  2sqlem8  15796  2sqlem10  15798  gropd  15842  grstructd2dom  15843  upgredg2vtx  15940  upgredgpr  15941  cbvrald  16110  bj-bdfindes  16270  bj-omtrans  16277  bj-inf2vnlem1  16291  bj-inf2vnlem2  16292  bj-inf2vnlem3  16293  bj-inf2vnlem4  16294  bj-findes  16302  strcoll2  16304  sscoll2  16309  subctctexmid  16325  pw1nct  16328  exmidsbthrlem  16349  sbthom  16353  apdiff  16375  ismkvnnlem  16379  nconstwlpolem  16392  neapmkv  16395  neap0mkv  16396  ltlenmkv  16397