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  1550  drnf1  1744  drnf2  1745  equveli  1770  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  mobidh  2072  mobid  2073  axext3  2172  cbvralfw  2708  cbvralf  2710  cbvralvw  2722  cbvraldva2  2725  gencbval  2800  vtoclgaf  2817  vtocl2gaf  2819  vtocl3gaf  2821  rspct  2849  rspc  2850  rspc2gv  2868  ceqex  2879  ralab2  2916  mob2  2932  mob  2934  morex  2936  reu7  2947  reu8  2948  nelrdva  2959  cdeqim  2970  sbcimg  3019  csbhypf  3110  cbvralcsf  3134  dfss2f  3161  sbcssg  3547  sneqrg  3777  elintab  3870  intss1  3874  intmin  3879  dfiin2g  3934  disji2  4011  disjiun  4013  trel  4123  trss  4125  bnd2  4191  zfpow  4193  exmidexmid  4214  exmidsssnc  4221  exmidundifim  4225  exmid1stab  4226  rext  4233  opth  4255  copsexg  4262  poeq1  4317  pocl  4321  swopolem  4323  swopo  4324  soeq1  4333  sowlin  4338  frforeq2  4363  frforeq3  4365  frirrg  4368  frind  4370  weeq1  4374  ordelord  4399  reusv3i  4477  ordtriexmid  4538  ontr2exmid  4542  onsucsssucexmid  4544  onsucelsucexmid  4547  ordsucunielexmid  4548  regexmidlem1  4550  regexmid  4552  reg2exmid  4553  elirr  4558  en2lp  4571  ordsoexmid  4579  onintexmid  4590  reg3exmid  4597  tfis  4600  tfisi  4604  peano2  4612  findes  4620  nnregexmid  4638  omsinds  4639  vtoclr  4692  poinxp  4713  soinxp  4714  posng  4716  ssrel  4732  ssrel2  4734  ssrelrel  4744  relop  4795  issref  5029  iotaexab  5214  iota5  5217  dffun4f  5251  sbcfung  5259  funopg  5269  brprcneu  5527  funfveu  5547  tz6.12f  5563  funbrfv  5575  ssimaexg  5599  fvmptss2  5612  fvmptssdm  5621  fvmptf  5629  fvelrn  5668  f1veqaeq  5791  dff13f  5792  isopolem  5844  isosolem  5846  riota5f  5877  imbrov2fvoveq  5922  oprabid  5929  ovmpos  6021  ov2gf  6022  ovi3  6034  caovcan  6062  caovordig  6063  caofrss  6132  caoftrn  6133  dfoprab4f  6219  f1o2ndf1  6254  poxp  6258  smoel  6326  tfrlem1  6334  tfr1onlemsucfn  6366  tfr1onlemsucaccv  6367  tfr1onlembxssdm  6369  tfr1onlembfn  6370  tfr1onlemaccex  6374  tfr1onlemres  6375  tfrcllemsucfn  6379  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllembfn  6383  tfrcllemaccex  6387  tfrcllemres  6388  tfrcl  6390  nnsucelsuc  6517  nnsucsssuc  6518  nnmordi  6542  nnaordex  6554  qsel  6639  eroveu  6653  ecopovtrn  6659  ecopovtrng  6662  th3qlem2  6665  ixpsnf1o  6763  fundmeng  6834  phplem3g  6885  nneneq  6886  ssfiexmid  6905  domfiexmid  6907  findcard  6917  findcard2  6918  findcard2s  6919  findcard2d  6920  findcard2sd  6921  diffifi  6923  ac6sfi  6927  fiintim  6958  fisseneq  6961  fidcenumlemrk  6984  fidcenumlemr  6985  isbth  6997  supeq3  7020  supeq123d  7021  supmoti  7023  suplubti  7030  supisolem  7038  cnvinfex  7048  eqinfti  7050  infvalti  7052  ordiso2  7065  nnnninfeq2  7158  isomni  7165  finomni  7169  exmidomni  7171  ctssexmid  7179  ismkv  7182  ismkvnex  7184  mkvprop  7187  fodjumkvlemres  7188  enmkvlem  7190  iswomni  7194  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  tapeq1  7282  exmidapne  7290  ccfunen  7294  ltsonq  7428  ltexnqq  7438  prcdnql  7514  prcunqu  7515  prloc  7521  prdisj  7522  genprndl  7551  genprndu  7552  caucvgprlemnkj  7696  caucvgprlemnbj  7697  caucvgprlemcl  7706  caucvgprprlemcbv  7717  caucvgprprlemval  7718  suplocexprlemloc  7751  lttrsr  7792  ltsosr  7794  recexgt0sr  7803  mulgt0sr  7808  aptisr  7809  mulextsr1  7811  srpospr  7813  caucvgsrlemgt1  7825  caucvgsrlemoffres  7830  caucvgsr  7832  map2psrprg  7835  suplocsrlemb  7836  axprecex  7910  axpre-ltwlin  7913  axpre-lttrn  7914  axpre-apti  7915  axpre-mulgt0  7917  axpre-mulext  7918  axcaucvglemcau  7928  axcaucvglemres  7929  axpre-suploclemres  7931  axpre-suploc  7932  axsuploc  8061  ltleletr  8070  ltordlem  8470  squeeze0  8892  sup3exmid  8945  nnsub  8989  fzind  9399  uzind4s  9622  uzind4s2  9623  indstr  9625  supinfneg  9627  infsupneg  9628  frec2uzuzd  10435  frec2uzltd  10436  uzsinds  10475  seq3fveq2  10502  seq3shft2  10506  monoord  10509  seq3split  10512  seq3id2  10542  expcl2lemap  10566  nn0ltexp2  10724  facdiv  10753  facwordi  10755  zfz1isolem1  10855  zfz1iso  10856  seq3coll  10857  caucvgre  11025  fimaxre2  11270  climcn1  11351  climcn2  11352  subcn2  11354  summodclem2a  11424  fsumsplitf  11451  fsum2d  11478  modfsummod  11501  fsumabs  11508  telfsumo  11509  fsumiun  11520  prodfdivap  11590  fprod2d  11666  fproddivapf  11674  fprodsplitf  11675  fprodsplit1f  11677  ndvdssub  11970  bezoutlemmain  12034  bezoutlemex  12037  bezoutlemzz  12038  bezoutlemsup  12045  dfgcd2  12050  algcvg  12083  algcvga  12086  algfx  12087  lcmgcdlem  12112  lcmdvds  12114  coprmgcdb  12123  coprmdvds1  12126  coprmdvds2  12128  prmind2  12155  dvdsprime  12157  nprm  12158  dvdsprm  12172  exprmfct  12173  isprm5lem  12176  coprm  12179  isprm6  12182  prmfac1  12187  sqrt2irr  12197  pcqmul  12338  pcqcl  12341  pc2dvds  12365  pcz  12367  prmpwdvds  12390  ennnfonelemim  12478  exmidunben  12480  infpn2  12510  setscomd  12556  mhmlem  13071  isnsg2  13159  ghmf1  13229  islring  13556  lringuplu  13560  uniopn  13978  fiinopn  13981  epttop  14067  cnpval  14175  iscnp  14176  icnpimaex  14188  lmcvg  14194  cnptoprest  14216  cnptoprest2  14217  lmss  14223  lmff  14226  txcnp  14248  txlm  14256  cnmpt12  14264  cnmpt22  14271  blssps  14404  blss  14405  metss  14471  comet  14476  metcnp3  14488  metcnp2  14490  txmetcnp  14495  divcnap  14532  elcncf2  14538  cncfi  14542  mulc1cncf  14553  cncfmet  14556  mulcncflem  14567  mulcncf  14568  dedekindeulemloc  14574  dedekindeulemlu  14576  dedekindeulemeu  14577  suplociccreex  14579  dedekindicclemloc  14583  dedekindicclemlu  14585  dedekindicclemeu  14586  ivthinclemlopn  14591  ivthinclemlr  14592  ivthinclemuopn  14593  ivthinclemur  14594  ivthinclemloc  14596  limccl  14605  ellimc3apf  14606  limccnpcntop  14621  limccnp2lem  14622  limccoap  14624  dvcoapbr  14648  lgsdir2lem4  14910  lgseisenlem2  14929  2sqlem6  14945  2sqlem8  14948  2sqlem10  14950  cbvrald  15018  bj-bdfindes  15179  bj-omtrans  15186  bj-inf2vnlem1  15200  bj-inf2vnlem2  15201  bj-inf2vnlem3  15202  bj-inf2vnlem4  15203  bj-findes  15211  strcoll2  15213  sscoll2  15218  subctctexmid  15229  pw1nct  15231  exmidsbthrlem  15249  sbthom  15253  apdiff  15275  ismkvnnlem  15279  nconstwlpolem  15292  neapmkv  15295  neap0mkv  15296  ltlenmkv  15297