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  840  nfbidf  1588  drnf1  1782  drnf2  1783  equveli  1808  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  mobidh  2116  mobid  2117  axext3  2217  cbvralfw  2769  cbvralf  2771  cbvralvw  2784  cbvraldva2  2787  gencbval  2865  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  rspct  2916  rspc  2917  rspc2gv  2936  ceqex  2947  ralab2  2984  mob2  3000  mob  3002  morex  3004  reu7  3015  reu8  3016  nelrdva  3027  cdeqim  3038  sbcimg  3087  csbhypf  3180  cbvralcsf  3204  dfssf  3232  dfss2f  3233  sbcssg  3622  ifeqeqxdc  3673  sneqrg  3871  elintab  3965  intss1  3969  intmin  3974  dfiin2g  4029  disji2  4106  disjiun  4109  trel  4220  trss  4222  bnd2  4291  zfpow  4293  exmidexmid  4314  exmidsssnc  4321  exmidundifim  4325  exmid1stab  4326  rext  4336  opth  4358  copsexg  4365  poeq1  4425  pocl  4429  swopolem  4431  swopo  4432  soeq1  4441  sowlin  4446  frforeq2  4471  frforeq3  4473  frirrg  4476  frind  4478  weeq1  4482  ordelord  4507  reusv3i  4585  ordtriexmid  4648  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  ordsucunielexmid  4658  regexmidlem1  4660  regexmid  4662  reg2exmid  4663  elirr  4668  en2lp  4681  ordsoexmid  4689  onintexmid  4700  reg3exmid  4707  tfis  4710  tfisi  4714  peano2  4722  findes  4730  nnregexmid  4748  omsinds  4749  vtoclr  4803  poinxp  4824  soinxp  4825  posng  4827  ssrel  4843  ssrel2  4845  ssrelrel  4855  relop  4910  issref  5150  iotaexab  5336  iota5  5339  dffun4f  5373  sbcfung  5381  funopg  5391  brprcneu  5668  funfveu  5688  tz6.12f  5704  funbrfv  5718  ssimaexg  5744  fvmptss2  5757  fvmptssdm  5767  fvmptf  5775  fvelrn  5813  f1veqaeq  5948  dff13f  5949  isopolem  6001  isosolem  6003  riota5f  6038  imbrov2fvoveq  6083  oprabid  6090  ovmpos  6185  ov2gf  6186  ovi3  6199  caovcan  6227  caovordig  6228  caofrss  6307  caoftrn  6308  dfoprab4f  6400  f1o2ndf1  6437  poxp  6441  suppfnss  6470  smoel  6544  tfrlem1  6552  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  nnsucelsuc  6737  nnsucsssuc  6738  nnmordi  6762  nnaordex  6774  qsel  6859  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem2  6885  ixpsnf1o  6984  fundmeng  7061  modom  7074  phplem3g  7123  nneneq  7124  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  findcard  7158  findcard2  7159  findcard2s  7160  findcard2d  7161  findcard2sd  7162  diffifi  7164  ac6sfi  7168  fiintim  7204  fisseneq  7208  fidcenumlemrk  7237  fidcenumlemr  7238  isbth  7250  supeq3  7294  supeq123d  7295  supmoti  7297  suplubti  7304  supisolem  7312  cnvinfex  7322  eqinfti  7324  infvalti  7326  ordiso2  7339  nninfninc  7427  nnnninfeq2  7433  isomni  7440  finomni  7444  exmidomni  7446  ctssexmid  7454  ismkv  7457  ismkvnex  7459  mkvprop  7462  fodjumkvlemres  7463  enmkvlem  7465  iswomni  7469  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  papeq1  7573  papsym  7576  papcotr  7577  tapeq1  7582  exmidapne  7590  ccfunen  7594  ltsonq  7729  ltexnqq  7739  prcdnql  7815  prcunqu  7816  prloc  7822  prdisj  7823  genprndl  7852  genprndu  7853  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemcl  8007  caucvgprprlemcbv  8018  caucvgprprlemval  8019  suplocexprlemloc  8052  lttrsr  8093  ltsosr  8095  recexgt0sr  8104  mulgt0sr  8109  aptisr  8110  mulextsr1  8112  srpospr  8114  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  map2psrprg  8136  suplocsrlemb  8137  axprecex  8211  axpre-ltwlin  8214  axpre-lttrn  8215  axpre-apti  8216  axpre-mulgt0  8218  axpre-mulext  8219  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  axsuploc  8362  ltleletr  8371  ltordlem  8774  squeeze0  9198  sup3exmid  9251  nnsub  9296  fzind  9714  uzind4s  9943  uzind4s2  9944  indstr  9946  supinfneg  9948  infsupneg  9949  frec2uzuzd  10791  frec2uzltd  10792  uzsinds  10833  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seqf1oglem2  10909  seqf1og  10910  seq3id2  10915  seqhomog  10919  expcl2lemap  10940  nn0ltexp2  11099  facdiv  11128  facwordi  11130  zfz1isolem1  11240  zfz1iso  11241  seq3coll  11242  wrdind  11442  wrd2ind  11443  swrdccatin1  11445  swrdccat3blem  11459  reuccatpfxs1lem  11466  caucvgre  11694  fimaxre2  11940  climcn1  12021  climcn2  12022  subcn2  12024  summodclem2a  12095  fsumsplitf  12122  fsum2d  12149  modfsummod  12172  fsumabs  12179  telfsumo  12180  fsumiun  12191  prodfdivap  12261  fprod2d  12337  fproddivapf  12345  fprodsplitf  12346  fprodsplit1f  12348  ndvdssub  12644  bezoutlemmain  12722  bezoutlemex  12725  bezoutlemzz  12726  bezoutlemsup  12733  dfgcd2  12738  algcvg  12773  algcvga  12776  algfx  12777  lcmgcdlem  12802  lcmdvds  12804  coprmgcdb  12813  coprmdvds1  12816  coprmdvds2  12818  prmind2  12845  dvdsprime  12847  nprm  12848  dvdsprm  12862  exprmfct  12863  isprm5lem  12866  coprm  12869  isprm6  12872  prmfac1  12877  sqrt2irr  12887  pcqmul  13029  pcqcl  13032  pc2dvds  13056  pcz  13058  prmpwdvds  13081  ballotfilem2  13175  ennnfonelemim  13262  exmidunben  13264  infpn2  13294  setscomd  13340  mhmlem  13870  isnsg2  13959  ghmf1  14029  islring  14440  lringuplu  14444  opprlring  14445  rrgval  14511  rrgeq0i  14513  isdomn  14519  domneq0  14522  opprdomnbg  14524  znidom  14934  znrrg  14937  mplvalcoe  14974  mplsubgfilemcl  14983  uniopn  14995  fiinopn  14998  epttop  15084  cnpval  15192  iscnp  15193  icnpimaex  15205  lmcvg  15211  cnptoprest  15233  cnptoprest2  15234  lmss  15240  lmff  15243  txcnp  15265  txlm  15273  cnmpt12  15281  cnmpt22  15288  blssps  15421  blss  15422  metss  15488  comet  15493  metcnp3  15505  metcnp2  15507  txmetcnp  15512  divcnap  15559  mpomulcn  15560  elcncf2  15568  cncfi  15572  mulc1cncf  15583  cncfmet  15586  mulcncflem  15601  mulcncf  15602  dedekindeulemloc  15613  dedekindeulemlu  15615  dedekindeulemeu  15616  suplociccreex  15618  dedekindicclemloc  15622  dedekindicclemlu  15624  dedekindicclemeu  15625  ivthinclemlopn  15630  ivthinclemlr  15631  ivthinclemuopn  15632  ivthinclemur  15633  ivthinclemloc  15635  ivthreinc  15639  limccl  15653  ellimc3apf  15654  limccnpcntop  15669  limccnp2lem  15670  limccoap  15672  dvcoapbr  15701  dvmptfsum  15719  mpodvdsmulf1o  15987  perfectlem2  15997  lgsdir2lem4  16033  gausslemma2dlem0i  16059  lgseisenlem2  16073  lgsquad2lem2  16084  2sqlem6  16122  2sqlem8  16125  2sqlem10  16127  gropd  16171  grstructd2dom  16172  upgredg2vtx  16272  upgredgpr  16273  eupth2fi  16603  lealltlt1  16634  lealltlt2  16635  dichmul0orlem7  16642  cbvrald  16699  bj-bdfindes  16858  bj-omtrans  16865  bj-inf2vnlem1  16879  bj-inf2vnlem2  16880  bj-inf2vnlem3  16881  bj-inf2vnlem4  16882  bj-findes  16890  strcoll2  16892  sscoll2  16897  subctctexmid  16913  pw1nct  16916  exmidnotnotr  16918  exmidcon  16919  exmidsbthrlem  16941  sbthom  16945  apdiff  16971  ismkvnnlem  16976  nconstwlpolem  16990  neapmkv  16993  neap0mkv  16994  ltlenmkv  16995