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  7330  supeq123d  7331  supmoti  7333  suplubti  7340  supisolem  7348  cnvinfex  7358  eqinfti  7360  infvalti  7362  ordiso2  7375  nninfninc  7463  nnnninfeq2  7469  isomni  7476  finomni  7480  exmidomni  7482  ctssexmid  7490  ismkv  7493  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  iswomni  7505  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papeq1  7609  papsym  7612  papcotr  7613  tapeq1  7618  exmidapne  7626  ccfunen  7630  ltsonq  7765  ltexnqq  7775  prcdnql  7851  prcunqu  7852  prloc  7858  prdisj  7859  genprndl  7888  genprndu  7889  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgprprlemcbv  8054  caucvgprprlemval  8055  suplocexprlemloc  8088  lttrsr  8129  ltsosr  8131  recexgt0sr  8140  mulgt0sr  8145  aptisr  8146  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  suplocsrlemb  8173  axprecex  8247  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  axsuploc  8398  ltleletr  8407  ltordlem  8810  squeeze0  9234  sup3exmid  9287  nnsub  9343  fzind  9761  uzind4s  9990  uzind4s2  9991  indstr  9993  supinfneg  9995  infsupneg  9996  frec2uzuzd  10839  frec2uzltd  10840  uzsinds  10881  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  seqf1oglem2  10957  seqf1og  10958  seq3id2  10963  seqhomog  10967  expcl2lemap  10988  nn0ltexp2  11147  facdiv  11176  facwordi  11178  zfz1isolem1  11292  zfz1iso  11293  seq3coll  11294  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  swrdccat3blem  11511  reuccatpfxs1lem  11518  caucvgre  11747  fimaxre2  11993  climcn1  12074  climcn2  12075  subcn2  12077  summodclem2a  12148  fsumsplitf  12175  fsum2d  12202  modfsummod  12225  fsumabs  12232  telfsumo  12233  fsumiun  12244  prodfdivap  12314  fprod2d  12390  fproddivapf  12398  fprodsplitf  12399  fprodsplit1f  12401  ndvdssub  12697  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemzz  12779  bezoutlemsup  12786  dfgcd2  12791  algcvg  12826  algcvga  12829  algfx  12830  lcmgcdlem  12855  lcmdvds  12857  coprmgcdb  12866  coprmdvds1  12869  coprmdvds2  12871  prmind2  12898  dvdsprime  12900  nprm  12901  dvdsprm  12915  exprmfct  12916  isprm5lem  12919  coprm  12922  isprm6  12925  prmfac1  12930  sqrt2irr  12940  pcqmul  13082  pcqcl  13085  pc2dvds  13109  pcz  13111  prmpwdvds  13134  ballotfilem2  13228  ennnfonelemim  13315  exmidunben  13317  infpn2  13347  setscomd  13393  mhmlem  13917  isnsg2  14006  ghmf1  14076  islring  14499  lringuplu  14503  opprlring  14504  rrgval  14570  rrgeq0i  14572  isdomn  14578  domneq0  14581  opprdomnbg  14583  znidom  14992  znrrg  14995  mplvalcoe  15081  mplsubgfilemcl  15090  uniopn  15102  fiinopn  15105  epttop  15191  cnpval  15299  iscnp  15300  icnpimaex  15312  lmcvg  15318  cnptoprest  15340  cnptoprest2  15341  lmss  15347  lmff  15350  txcnp  15372  txlm  15380  cnmpt12  15388  cnmpt22  15395  blssps  15528  blss  15529  metss  15595  comet  15600  metcnp3  15612  metcnp2  15614  txmetcnp  15619  divcnap  15666  mpomulcn  15667  elcncf2  15675  cncfi  15679  mulc1cncf  15690  cncfmet  15693  mulcncflem  15708  mulcncf  15709  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeulemeu  15723  suplociccreex  15725  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicclemeu  15732  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthreinc  15746  limccl  15760  ellimc3apf  15761  limccnpcntop  15776  limccnp2lem  15777  limccoap  15779  dvcoapbr  15808  dvmptfsum  15826  mpodvdsmulf1o  16104  perfectlem2  16114  lgsdir2lem4  16150  gausslemma2dlem0i  16176  lgseisenlem2  16190  lgsquad2lem2  16201  2sqlem6  16239  2sqlem8  16242  2sqlem10  16244  gropd  16288  grstructd2dom  16289  upgredg2vtx  16389  upgredgpr  16390  eupth2fi  16720  lealltlt1  16751  lealltlt2  16752  dichmul0orlem7  16759  cbvrald  16816  bj-bdfindes  16975  bj-omtrans  16982  bj-inf2vnlem1  16996  bj-inf2vnlem2  16997  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999  bj-findes  17007  strcoll2  17009  sscoll2  17014  subctctexmid  17030  pw1nct  17033  exmidnotnotr  17036  exmidcon  17037  wexmiddiffilem  17043  wexmiddifxy  17046  exmidsbthrlem  17067  sbthom  17071  apdiff  17097  ismkvnnlem  17102  nconstwlpolem  17115  neapmkv  17118  neap0mkv  17119  ltlenmkv  17120  alsbid  17143  cbvals  17146