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 ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  stbid  844  nfbidf  1592  drnf1  1786  drnf2  1787  equveli  1812  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  mobidh  2120  mobid  2121  axext3  2221  cbvralfw  2775  cbvralf  2777  cbvralvw  2790  cbvraldva2  2793  gencbval  2871  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  rspc2gv  2942  ceqex  2953  ralab2  2990  mob2  3006  mob  3008  morex  3010  reu7  3021  reu8  3022  nelrdva  3033  cdeqim  3044  sbcimg  3093  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  sbcssg  3636  ifeqeqxdc  3687  sneqrg  3887  elintab  3981  intss1  3985  intmin  3990  dfiin2g  4045  disji2  4122  disjiun  4125  trel  4236  trss  4238  bnd2  4310  zfpow  4312  exmidexmid  4333  exmidsssnc  4340  exmidundifim  4344  exmid1stab  4345  rext  4355  opth  4377  copsexg  4384  poeq1  4444  pocl  4448  swopolem  4450  swopo  4451  soeq1  4460  sowlin  4465  frforeq2  4490  frforeq3  4492  frirrg  4495  frind  4497  weeq1  4501  ordelord  4526  reusv3i  4605  ordtriexmid  4668  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  regexmid  4682  reg2exmid  4683  elirr  4688  en2lp  4701  ordsoexmid  4709  onintexmid  4720  reg3exmid  4727  tfis  4730  tfisi  4734  peano2  4742  findes  4750  nnregexmid  4768  omsinds  4769  vtoclr  4823  poinxp  4844  soinxp  4845  posng  4847  ssrel  4863  ssrel2  4865  ssrelrel  4875  relop  4930  issref  5170  iotaexab  5356  iota5  5359  dffun4f  5393  sbcfung  5401  funopg  5411  brprcneu  5688  funfveu  5708  tz6.12f  5724  funbrfv  5739  ssimaexg  5765  fvmptss2  5780  fvmptssdm  5790  fvmptf  5798  fvelrn  5839  f1veqaeq  5975  dff13f  5976  isopolem  6028  isosolem  6030  riota5f  6065  imbrov2fvoveq  6110  oprabid  6117  ovmpos  6212  ov2gf  6213  ovi3  6226  caovcan  6254  caovordig  6255  caofrss  6334  caoftrn  6335  dfoprab4f  6427  f1o2ndf1  6464  poxp  6468  suppfnss  6497  smoel  6571  tfrlem1  6579  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  nnsucelsuc  6764  nnsucsssuc  6765  nnmordi  6789  nnaordex  6801  qsel  6886  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  ixpsnf1o  7018  fundmeng  7095  modom  7108  phplem3g  7157  nneneq  7158  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  diffifi  7198  ac6sfi  7202  fiintim  7238  fisseneq  7242  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  supeq3  7331  supeq123d  7332  supmoti  7334  suplubti  7341  supisolem  7349  cnvinfex  7359  eqinfti  7361  infvalti  7363  ordiso2  7376  nninfninc  7464  nnnninfeq2  7470  isomni  7477  finomni  7481  exmidomni  7483  ctssexmid  7491  ismkv  7494  ismkvnex  7496  mkvprop  7499  fodjumkvlemres  7500  enmkvlem  7502  iswomni  7506  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  papeq1  7610  papsym  7613  papcotr  7614  tapeq1  7619  exmidapne  7627  ccfunen  7631  ltsonq  7766  ltexnqq  7776  prcdnql  7852  prcunqu  7853  prloc  7859  prdisj  7860  genprndl  7889  genprndu  7890  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemcl  8044  caucvgprprlemcbv  8055  caucvgprprlemval  8056  suplocexprlemloc  8089  lttrsr  8130  ltsosr  8132  recexgt0sr  8141  mulgt0sr  8146  aptisr  8147  mulextsr1  8149  srpospr  8151  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  map2psrprg  8173  suplocsrlemb  8174  axprecex  8248  axpre-ltwlin  8251  axpre-lttrn  8252  axpre-apti  8253  axpre-mulgt0  8255  axpre-mulext  8256  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  axsuploc  8399  ltleletr  8408  ltordlem  8812  squeeze0  9237  sup3exmid  9290  nnsub  9346  fzind  9766  uzind4s  10000  uzind4s2  10001  indstr  10003  supinfneg  10005  infsupneg  10006  frec2uzuzd  10854  frec2uzltd  10855  uzsinds  10896  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seqf1oglem2  10972  seqf1og  10973  seq3id2  10978  seqhomog  10982  expcl2lemap  11003  nn0ltexp2  11163  facdiv  11192  facwordi  11194  zfz1isolem1  11308  zfz1iso  11309  seq3coll  11310  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  swrdccat3blem  11527  reuccatpfxs1lem  11534  caucvgre  11763  fimaxre2  12010  climcn1  12093  climcn2  12094  subcn2  12096  summodclem2a  12167  fsumsplitf  12194  fsum2d  12221  modfsummod  12244  fsumabs  12251  telfsumo  12252  fsumiun  12263  prodfdivap  12333  fprod2d  12409  fproddivapf  12417  fprodsplitf  12418  fprodsplit1f  12420  ndvdssub  12716  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemzz  12798  bezoutlemsup  12805  dfgcd2  12810  algcvg  12845  algcvga  12848  algfx  12849  lcmgcdlem  12874  lcmdvds  12876  coprmgcdb  12885  coprmdvds1  12888  coprmdvds2  12890  prmind2  12917  dvdsprime  12919  nprm  12920  dvdsprm  12935  exprmfct  12936  isprm5lem  12939  coprm  12942  isprm6  12945  prmfac1  12950  sqrt2irr  12960  pcqmul  13105  pcqcl  13108  pc2dvds  13132  pcz  13134  prmpwdvds  13157  prmlem0  13243  ballotfilem2  13280  ennnfonelemim  13367  exmidunben  13369  infpn2  13399  setscomd  13445  mhmlem  13970  isnsg2  14059  ghmf1  14129  islring  14583  lringuplu  14587  opprlring  14588  rrgval  14654  rrgeq0i  14656  isdomn  14662  domneq0  14665  opprdomnbg  14667  znidom  15076  znrrg  15079  mplvalcoe  15172  mplsubgfilemcl  15181  uniopn  15193  fiinopn  15196  epttop  15282  cnpval  15390  iscnp  15391  icnpimaex  15403  lmcvg  15409  cnptoprest  15431  cnptoprest2  15432  lmss  15438  lmff  15441  txcnp  15463  txlm  15471  cnmpt12  15479  cnmpt22  15486  blssps  15619  blss  15620  metss  15686  comet  15691  metcnp3  15703  metcnp2  15705  txmetcnp  15710  divcnap  15757  mpomulcn  15758  elcncf2  15766  cncfi  15770  mulc1cncf  15781  cncfmet  15784  mulcncflem  15799  mulcncf  15800  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeulemeu  15814  suplociccreex  15816  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicclemeu  15823  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthreinc  15837  limccl  15851  ellimc3apf  15852  limccnpcntop  15867  limccnp2lem  15868  limccoap  15870  dvcoapbr  15899  dvmptfsum  15917  mpodvdsmulf1o  16245  perfectlem2  16261  bcmono  16265  lgsdir2lem4  16316  gausslemma2dlem0i  16342  lgseisenlem2  16356  lgsquad2lem2  16367  2sqlem6  16405  2sqlem8  16408  2sqlem10  16410  gropd  16454  grstructd2dom  16455  upgredg2vtx  16555  upgredgpr  16556  eupth2fi  16886  lealltlt1  16917  lealltlt2  16918  dichmul0orlem7  16925  cbvrald  16982  bj-bdfindes  17141  bj-omtrans  17148  bj-inf2vnlem1  17162  bj-inf2vnlem2  17163  bj-inf2vnlem3  17164  bj-inf2vnlem4  17165  bj-findes  17173  strcoll2  17175  sscoll2  17180  subctctexmid  17196  pw1nct  17199  exmidnotnotr  17202  exmidcon  17203  wexmiddiffilem  17209  wexmiddifxy  17212  exmidsbthrlem  17233  sbthom  17237  apdiff  17264  ismkvnnlem  17269  nconstwlpolem  17282  neapmkv  17285  neap0mkv  17286  ltlenmkv  17287  alsbid  17310  cbvals  17313