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  2850  vtoclgaf  2867  vtocl2gaf  2869  vtocl3gaf  2871  rspct  2901  rspc  2902  rspc2gv  2920  ceqex  2931  ralab2  2968  mob2  2984  mob  2986  morex  2988  reu7  2999  reu8  3000  nelrdva  3011  cdeqim  3022  sbcimg  3071  csbhypf  3164  cbvralcsf  3188  dfss2f  3216  sbcssg  3601  sneqrg  3843  elintab  3937  intss1  3941  intmin  3946  dfiin2g  4001  disji2  4078  disjiun  4081  trel  4192  trss  4194  bnd2  4261  zfpow  4263  exmidexmid  4284  exmidsssnc  4291  exmidundifim  4295  exmid1stab  4296  rext  4305  opth  4327  copsexg  4334  poeq1  4394  pocl  4398  swopolem  4400  swopo  4401  soeq1  4410  sowlin  4415  frforeq2  4440  frforeq3  4442  frirrg  4445  frind  4447  weeq1  4451  ordelord  4476  reusv3i  4554  ordtriexmid  4617  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  ordsucunielexmid  4627  regexmidlem1  4629  regexmid  4631  reg2exmid  4632  elirr  4637  en2lp  4650  ordsoexmid  4658  onintexmid  4669  reg3exmid  4676  tfis  4679  tfisi  4683  peano2  4691  findes  4699  nnregexmid  4717  omsinds  4718  vtoclr  4772  poinxp  4793  soinxp  4794  posng  4796  ssrel  4812  ssrel2  4814  ssrelrel  4824  relop  4878  issref  5117  iotaexab  5303  iota5  5306  dffun4f  5340  sbcfung  5348  funopg  5358  brprcneu  5628  funfveu  5648  tz6.12f  5664  funbrfv  5678  ssimaexg  5704  fvmptss2  5717  fvmptssdm  5727  fvmptf  5735  fvelrn  5774  f1veqaeq  5905  dff13f  5906  isopolem  5958  isosolem  5960  riota5f  5993  imbrov2fvoveq  6038  oprabid  6045  ovmpos  6140  ov2gf  6141  ovi3  6154  caovcan  6182  caovordig  6183  caofrss  6262  caoftrn  6263  dfoprab4f  6351  f1o2ndf1  6388  poxp  6392  smoel  6461  tfrlem1  6469  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  nnsucelsuc  6654  nnsucsssuc  6655  nnmordi  6679  nnaordex  6691  qsel  6776  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem2  6802  ixpsnf1o  6900  fundmeng  6977  modom  6989  phplem3g  7037  nneneq  7038  ssfiexmid  7058  domfiexmid  7060  findcard  7070  findcard2  7071  findcard2s  7072  findcard2d  7073  findcard2sd  7074  diffifi  7076  ac6sfi  7080  fiintim  7116  fisseneq  7119  fidcenumlemrk  7144  fidcenumlemr  7145  isbth  7157  supeq3  7180  supeq123d  7181  supmoti  7183  suplubti  7190  supisolem  7198  cnvinfex  7208  eqinfti  7210  infvalti  7212  ordiso2  7225  nninfninc  7313  nnnninfeq2  7319  isomni  7326  finomni  7330  exmidomni  7332  ctssexmid  7340  ismkv  7343  ismkvnex  7345  mkvprop  7348  fodjumkvlemres  7349  enmkvlem  7351  iswomni  7355  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  tapeq1  7461  exmidapne  7469  ccfunen  7473  ltsonq  7608  ltexnqq  7618  prcdnql  7694  prcunqu  7695  prloc  7701  prdisj  7702  genprndl  7731  genprndu  7732  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemcl  7886  caucvgprprlemcbv  7897  caucvgprprlemval  7898  suplocexprlemloc  7931  lttrsr  7972  ltsosr  7974  recexgt0sr  7983  mulgt0sr  7988  aptisr  7989  mulextsr1  7991  srpospr  7993  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  caucvgsr  8012  map2psrprg  8015  suplocsrlemb  8016  axprecex  8090  axpre-ltwlin  8093  axpre-lttrn  8094  axpre-apti  8095  axpre-mulgt0  8097  axpre-mulext  8098  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  axsuploc  8242  ltleletr  8251  ltordlem  8652  squeeze0  9074  sup3exmid  9127  nnsub  9172  fzind  9585  uzind4s  9814  uzind4s2  9815  indstr  9817  supinfneg  9819  infsupneg  9820  frec2uzuzd  10654  frec2uzltd  10655  uzsinds  10696  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  seqf1oglem2  10772  seqf1og  10773  seq3id2  10778  seqhomog  10782  expcl2lemap  10803  nn0ltexp2  10961  facdiv  10990  facwordi  10992  zfz1isolem1  11094  zfz1iso  11095  seq3coll  11096  wrdind  11293  wrd2ind  11294  swrdccatin1  11296  swrdccat3blem  11310  reuccatpfxs1lem  11317  caucvgre  11532  fimaxre2  11778  climcn1  11859  climcn2  11860  subcn2  11862  summodclem2a  11932  fsumsplitf  11959  fsum2d  11986  modfsummod  12009  fsumabs  12016  telfsumo  12017  fsumiun  12028  prodfdivap  12098  fprod2d  12174  fproddivapf  12182  fprodsplitf  12183  fprodsplit1f  12185  ndvdssub  12481  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemzz  12563  bezoutlemsup  12570  dfgcd2  12575  algcvg  12610  algcvga  12613  algfx  12614  lcmgcdlem  12639  lcmdvds  12641  coprmgcdb  12650  coprmdvds1  12653  coprmdvds2  12655  prmind2  12682  dvdsprime  12684  nprm  12685  dvdsprm  12699  exprmfct  12700  isprm5lem  12703  coprm  12706  isprm6  12709  prmfac1  12714  sqrt2irr  12724  pcqmul  12866  pcqcl  12869  pc2dvds  12893  pcz  12895  prmpwdvds  12918  ennnfonelemim  13035  exmidunben  13037  infpn2  13067  setscomd  13113  mhmlem  13691  isnsg2  13780  ghmf1  13850  islring  14196  lringuplu  14200  rrgval  14266  rrgeq0i  14268  isdomn  14273  domneq0  14276  opprdomnbg  14278  znidom  14661  znrrg  14664  mplvalcoe  14694  mplsubgfilemcl  14703  uniopn  14715  fiinopn  14718  epttop  14804  cnpval  14912  iscnp  14913  icnpimaex  14925  lmcvg  14931  cnptoprest  14953  cnptoprest2  14954  lmss  14960  lmff  14963  txcnp  14985  txlm  14993  cnmpt12  15001  cnmpt22  15008  blssps  15141  blss  15142  metss  15208  comet  15213  metcnp3  15225  metcnp2  15227  txmetcnp  15232  divcnap  15279  mpomulcn  15280  elcncf2  15288  cncfi  15292  mulc1cncf  15303  cncfmet  15306  mulcncflem  15321  mulcncf  15322  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeulemeu  15336  suplociccreex  15338  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemeu  15345  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthreinc  15359  limccl  15373  ellimc3apf  15374  limccnpcntop  15389  limccnp2lem  15390  limccoap  15392  dvcoapbr  15421  dvmptfsum  15439  mpodvdsmulf1o  15704  perfectlem2  15714  lgsdir2lem4  15750  gausslemma2dlem0i  15776  lgseisenlem2  15790  lgsquad2lem2  15801  2sqlem6  15839  2sqlem8  15842  2sqlem10  15844  gropd  15888  grstructd2dom  15889  upgredg2vtx  15987  upgredgpr  15988  cbvrald  16320  bj-bdfindes  16480  bj-omtrans  16487  bj-inf2vnlem1  16501  bj-inf2vnlem2  16502  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504  bj-findes  16512  strcoll2  16514  sscoll2  16519  subctctexmid  16537  pw1nct  16540  exmidsbthrlem  16562  sbthom  16566  apdiff  16588  ismkvnnlem  16592  nconstwlpolem  16605  neapmkv  16608  neap0mkv  16609  ltlenmkv  16610