Theorem imbi12d 233

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 230	. 2 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	imbi2d 229	. 2 |- ( ph -> ( ( ch -> th ) <-> ( ch -> ta ) ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  783  nfbidf  1487  drnf1  1679  drnf2  1680  equveli  1700  ax11v2  1759  ax11v  1766  ax11ev  1767  equs5or  1769  mobidh  1994  mobid  1995  axext3  2083  cbvralf  2606  cbvraldva2  2616  gencbval  2689  vtoclgaf  2706  vtocl2gaf  2708  vtocl3gaf  2710  rspct  2737  rspc  2738  rspc2gv  2755  ceqex  2766  ralab2  2801  mob2  2817  mob  2819  morex  2821  reu7  2832  reu8  2833  nelrdva  2844  cdeqim  2855  sbcimg  2902  csbhypf  2988  cbvralcsf  3012  dfss2f  3038  sbcssg  3419  sneqrg  3636  elintab  3729  intss1  3733  intmin  3738  dfiin2g  3793  disji2  3868  disjiun  3870  trel  3973  trss  3975  bnd2  4037  zfpow  4039  exmidexmid  4060  exmidsssnc  4064  exmidundifim  4068  rext  4075  opth  4097  copsexg  4104  poeq1  4159  pocl  4163  swopolem  4165  swopo  4166  soeq1  4175  sowlin  4180  frforeq2  4205  frforeq3  4207  frirrg  4210  frind  4212  weeq1  4216  ordelord  4241  reusv3i  4318  ordtriexmid  4375  ontr2exmid  4378  onsucsssucexmid  4380  onsucelsucexmid  4383  ordsucunielexmid  4384  regexmidlem1  4386  regexmid  4388  reg2exmid  4389  elirr  4394  en2lp  4407  ordsoexmid  4415  onintexmid  4425  reg3exmid  4432  tfis  4435  tfisi  4439  peano2  4447  findes  4455  nnregexmid  4472  omsinds  4473  vtoclr  4525  poinxp  4546  soinxp  4547  posng  4549  ssrel  4565  ssrel2  4567  ssrelrel  4577  relop  4627  issref  4857  iota5  5044  dffun4f  5075  sbcfung  5083  funopg  5093  brprcneu  5346  funfveu  5366  tz6.12f  5382  funbrfv  5392  ssimaexg  5415  fvmptss2  5428  fvmptssdm  5437  fvmptf  5445  fvelrn  5483  f1veqaeq  5602  dff13f  5603  isopolem  5655  isosolem  5657  riota5f  5686  imbrov2fvoveq  5731  oprabid  5735  ovmpos  5826  ov2gf  5827  ovi3  5839  caovcan  5867  caovordig  5868  caofrss  5937  caoftrn  5938  dfoprab4f  6021  f1o2ndf1  6055  poxp  6059  smoel  6127  tfrlem1  6135  tfr1onlemsucfn  6167  tfr1onlemsucaccv  6168  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfr1onlemaccex  6175  tfr1onlemres  6176  tfrcllemsucfn  6180  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllembfn  6184  tfrcllemaccex  6188  tfrcllemres  6189  tfrcl  6191  nnsucelsuc  6317  nnsucsssuc  6318  nnmordi  6342  nnaordex  6353  qsel  6436  eroveu  6450  ecopovtrn  6456  ecopovtrng  6459  th3qlem2  6462  ixpsnf1o  6560  fundmeng  6631  phplem3g  6679  nneneq  6680  ssfiexmid  6699  domfiexmid  6701  findcard  6711  findcard2  6712  findcard2s  6713  findcard2d  6714  findcard2sd  6715  diffifi  6717  ac6sfi  6721  fiintim  6746  fisseneq  6749  fidcenumlemrk  6770  fidcenumlemr  6771  isbth  6783  supeq3  6792  supeq123d  6793  supmoti  6795  suplubti  6802  supisolem  6810  cnvinfex  6820  eqinfti  6822  infvalti  6824  ordiso2  6835  isomni  6920  finomni  6924  exmidomni  6926  ctssexmid  6936  ismkv  6939  mkvprop  6943  fodjumkvlemres  6944  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  ltsonq  7107  ltexnqq  7117  prcdnql  7193  prcunqu  7194  prloc  7200  prdisj  7201  genprndl  7230  genprndu  7231  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemcl  7385  caucvgprprlemcbv  7396  caucvgprprlemval  7397  lttrsr  7458  ltsosr  7460  recexgt0sr  7469  mulgt0sr  7473  aptisr  7474  mulextsr1  7476  srpospr  7478  caucvgsrlemgt1  7490  caucvgsrlemoffres  7495  caucvgsr  7497  axprecex  7565  axpre-ltwlin  7568  axpre-lttrn  7569  axpre-apti  7570  axpre-mulgt0  7572  axpre-mulext  7573  axcaucvglemcau  7583  axcaucvglemres  7584  ltleletr  7717  ltordlem  8111  squeeze0  8520  sup3exmid  8573  nnsub  8617  fzind  9018  uzind4s  9235  uzind4s2  9236  indstr  9238  supinfneg  9240  infsupneg  9241  frec2uzuzd  10016  frec2uzltd  10017  uzsinds  10056  seq3fveq2  10083  seq3shft2  10087  monoord  10090  seq3split  10093  seq3id2  10123  expcl2lemap  10146  facdiv  10325  facwordi  10327  zfz1isolem1  10424  zfz1iso  10425  seq3coll  10426  caucvgre  10593  fimaxre2  10837  climcn1  10916  climcn2  10917  subcn2  10919  summodclem2a  10989  fsumsplitf  11016  fsum2d  11043  modfsummod  11066  fsumabs  11073  telfsumo  11074  fsumiun  11085  ndvdssub  11422  bezoutlemmain  11479  bezoutlemex  11482  bezoutlemzz  11483  bezoutlemsup  11490  dfgcd2  11495  algcvg  11522  algcvga  11525  algfx  11526  lcmgcdlem  11551  lcmdvds  11553  coprmgcdb  11562  coprmdvds1  11565  coprmdvds2  11567  prmind2  11594  dvdsprime  11596  nprm  11597  dvdsprm  11610  exprmfct  11611  coprm  11615  isprm6  11618  prmfac1  11623  sqrt2irr  11633  ennnfonelemim  11729  exmidunben  11731  uniopn  11950  fiinopn  11953  epttop  12041  cnpval  12148  iscnp  12149  icnpimaex  12161  lmcvg  12167  cnptoprest  12189  cnptoprest2  12190  lmss  12196  lmff  12199  txcnp  12221  txlm  12229  cnmpt12  12237  cnmpt22  12244  blssps  12355  blss  12356  metss  12422  comet  12427  metcnp3  12435  metcnp2  12437  elcncf2  12474  cncfi  12478  mulc1cncf  12489  cncfmet  12492  mulcncflem  12502  mulcncf  12503  limccl  12510  ellimc3ap  12511  limccnpcntop  12520  cbvrald  12576  bj-bdfindes  12732  bj-omtrans  12739  bj-inf2vnlem1  12753  bj-inf2vnlem2  12754  bj-inf2vnlem3  12755  bj-inf2vnlem4  12756  bj-findes  12764  strcoll2  12766  sscoll2  12771  exmidsbthrlem  12801  sbthom  12805