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  832  nfbidf  1539  drnf1  1733  drnf2  1734  equveli  1759  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  mobidh  2060  mobid  2061  axext3  2160  cbvralfw  2695  cbvralf  2697  cbvralvw  2709  cbvraldva2  2712  gencbval  2787  vtoclgaf  2804  vtocl2gaf  2806  vtocl3gaf  2808  rspct  2836  rspc  2837  rspc2gv  2855  ceqex  2866  ralab2  2903  mob2  2919  mob  2921  morex  2923  reu7  2934  reu8  2935  nelrdva  2946  cdeqim  2957  sbcimg  3006  csbhypf  3097  cbvralcsf  3121  dfss2f  3148  sbcssg  3534  sneqrg  3764  elintab  3857  intss1  3861  intmin  3866  dfiin2g  3921  disji2  3998  disjiun  4000  trel  4110  trss  4112  bnd2  4175  zfpow  4177  exmidexmid  4198  exmidsssnc  4205  exmidundifim  4209  exmid1stab  4210  rext  4217  opth  4239  copsexg  4246  poeq1  4301  pocl  4305  swopolem  4307  swopo  4308  soeq1  4317  sowlin  4322  frforeq2  4347  frforeq3  4349  frirrg  4352  frind  4354  weeq1  4358  ordelord  4383  reusv3i  4461  ordtriexmid  4522  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmid  4531  ordsucunielexmid  4532  regexmidlem1  4534  regexmid  4536  reg2exmid  4537  elirr  4542  en2lp  4555  ordsoexmid  4563  onintexmid  4574  reg3exmid  4581  tfis  4584  tfisi  4588  peano2  4596  findes  4604  nnregexmid  4622  omsinds  4623  vtoclr  4676  poinxp  4697  soinxp  4698  posng  4700  ssrel  4716  ssrel2  4718  ssrelrel  4728  relop  4779  issref  5013  iota5  5200  dffun4f  5234  sbcfung  5242  funopg  5252  brprcneu  5510  funfveu  5530  tz6.12f  5546  funbrfv  5556  ssimaexg  5580  fvmptss2  5593  fvmptssdm  5602  fvmptf  5610  fvelrn  5649  f1veqaeq  5772  dff13f  5773  isopolem  5825  isosolem  5827  riota5f  5857  imbrov2fvoveq  5902  oprabid  5909  ovmpos  6000  ov2gf  6001  ovi3  6013  caovcan  6041  caovordig  6042  caofrss  6109  caoftrn  6110  dfoprab4f  6196  f1o2ndf1  6231  poxp  6235  smoel  6303  tfrlem1  6311  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  nnsucelsuc  6494  nnsucsssuc  6495  nnmordi  6519  nnaordex  6531  qsel  6614  eroveu  6628  ecopovtrn  6634  ecopovtrng  6637  th3qlem2  6640  ixpsnf1o  6738  fundmeng  6809  phplem3g  6858  nneneq  6859  ssfiexmid  6878  domfiexmid  6880  findcard  6890  findcard2  6891  findcard2s  6892  findcard2d  6893  findcard2sd  6894  diffifi  6896  ac6sfi  6900  fiintim  6930  fisseneq  6933  fidcenumlemrk  6955  fidcenumlemr  6956  isbth  6968  supeq3  6991  supeq123d  6992  supmoti  6994  suplubti  7001  supisolem  7009  cnvinfex  7019  eqinfti  7021  infvalti  7023  ordiso2  7036  nnnninfeq2  7129  isomni  7136  finomni  7140  exmidomni  7142  ctssexmid  7150  ismkv  7153  ismkvnex  7155  mkvprop  7158  fodjumkvlemres  7159  enmkvlem  7161  iswomni  7165  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  tapeq1  7253  exmidapne  7261  ccfunen  7265  ltsonq  7399  ltexnqq  7409  prcdnql  7485  prcunqu  7486  prloc  7492  prdisj  7493  genprndl  7522  genprndu  7523  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemcl  7677  caucvgprprlemcbv  7688  caucvgprprlemval  7689  suplocexprlemloc  7722  lttrsr  7763  ltsosr  7765  recexgt0sr  7774  mulgt0sr  7779  aptisr  7780  mulextsr1  7782  srpospr  7784  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  caucvgsr  7803  map2psrprg  7806  suplocsrlemb  7807  axprecex  7881  axpre-ltwlin  7884  axpre-lttrn  7885  axpre-apti  7886  axpre-mulgt0  7888  axpre-mulext  7889  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  axsuploc  8032  ltleletr  8041  ltordlem  8441  squeeze0  8863  sup3exmid  8916  nnsub  8960  fzind  9370  uzind4s  9592  uzind4s2  9593  indstr  9595  supinfneg  9597  infsupneg  9598  frec2uzuzd  10404  frec2uzltd  10405  uzsinds  10444  seq3fveq2  10471  seq3shft2  10475  monoord  10478  seq3split  10481  seq3id2  10511  expcl2lemap  10534  nn0ltexp2  10691  facdiv  10720  facwordi  10722  zfz1isolem1  10822  zfz1iso  10823  seq3coll  10824  caucvgre  10992  fimaxre2  11237  climcn1  11318  climcn2  11319  subcn2  11321  summodclem2a  11391  fsumsplitf  11418  fsum2d  11445  modfsummod  11468  fsumabs  11475  telfsumo  11476  fsumiun  11487  prodfdivap  11557  fprod2d  11633  fproddivapf  11641  fprodsplitf  11642  fprodsplit1f  11644  ndvdssub  11937  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemzz  12005  bezoutlemsup  12012  dfgcd2  12017  algcvg  12050  algcvga  12053  algfx  12054  lcmgcdlem  12079  lcmdvds  12081  coprmgcdb  12090  coprmdvds1  12093  coprmdvds2  12095  prmind2  12122  dvdsprime  12124  nprm  12125  dvdsprm  12139  exprmfct  12140  isprm5lem  12143  coprm  12146  isprm6  12149  prmfac1  12154  sqrt2irr  12164  pcqmul  12305  pcqcl  12308  pc2dvds  12331  pcz  12333  prmpwdvds  12355  ennnfonelemim  12427  exmidunben  12429  infpn2  12459  setscomd  12505  mhmlem  12983  isnsg2  13068  islring  13338  lringuplu  13342  uniopn  13540  fiinopn  13543  epttop  13629  cnpval  13737  iscnp  13738  icnpimaex  13750  lmcvg  13756  cnptoprest  13778  cnptoprest2  13779  lmss  13785  lmff  13788  txcnp  13810  txlm  13818  cnmpt12  13826  cnmpt22  13833  blssps  13966  blss  13967  metss  14033  comet  14038  metcnp3  14050  metcnp2  14052  txmetcnp  14057  divcnap  14094  elcncf2  14100  cncfi  14104  mulc1cncf  14115  cncfmet  14118  mulcncflem  14129  mulcncf  14130  dedekindeulemloc  14136  dedekindeulemlu  14138  dedekindeulemeu  14139  suplociccreex  14141  dedekindicclemloc  14145  dedekindicclemlu  14147  dedekindicclemeu  14148  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemloc  14158  limccl  14167  ellimc3apf  14168  limccnpcntop  14183  limccnp2lem  14184  limccoap  14186  dvcoapbr  14210  lgsdir2lem4  14471  lgseisenlem2  14490  2sqlem6  14506  2sqlem8  14509  2sqlem10  14511  cbvrald  14579  bj-bdfindes  14740  bj-omtrans  14747  bj-inf2vnlem1  14761  bj-inf2vnlem2  14762  bj-inf2vnlem3  14763  bj-inf2vnlem4  14764  bj-findes  14772  strcoll2  14774  sscoll2  14779  subctctexmid  14789  pw1nct  14791  exmidsbthrlem  14809  sbthom  14813  apdiff  14835  ismkvnnlem  14839  nconstwlpolem  14852  neapmkv  14855  neap0mkv  14856  ltlenmkv  14857