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  839  nfbidf  1587  drnf1  1781  drnf2  1782  equveli  1807  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  mobidh  2113  mobid  2114  axext3  2214  cbvralfw  2756  cbvralf  2758  cbvralvw  2771  cbvraldva2  2774  gencbval  2852  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  rspc2gv  2922  ceqex  2933  ralab2  2970  mob2  2986  mob  2988  morex  2990  reu7  3001  reu8  3002  nelrdva  3013  cdeqim  3024  sbcimg  3073  csbhypf  3166  cbvralcsf  3190  dfss2f  3218  sbcssg  3603  sneqrg  3845  elintab  3939  intss1  3943  intmin  3948  dfiin2g  4003  disji2  4080  disjiun  4083  trel  4194  trss  4196  bnd2  4263  zfpow  4265  exmidexmid  4286  exmidsssnc  4293  exmidundifim  4297  exmid1stab  4298  rext  4307  opth  4329  copsexg  4336  poeq1  4396  pocl  4400  swopolem  4402  swopo  4403  soeq1  4412  sowlin  4417  frforeq2  4442  frforeq3  4444  frirrg  4447  frind  4449  weeq1  4453  ordelord  4478  reusv3i  4556  ordtriexmid  4619  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  regexmid  4633  reg2exmid  4634  elirr  4639  en2lp  4652  ordsoexmid  4660  onintexmid  4671  reg3exmid  4678  tfis  4681  tfisi  4685  peano2  4693  findes  4701  nnregexmid  4719  omsinds  4720  vtoclr  4774  poinxp  4795  soinxp  4796  posng  4798  ssrel  4814  ssrel2  4816  ssrelrel  4826  relop  4880  issref  5119  iotaexab  5305  iota5  5308  dffun4f  5342  sbcfung  5350  funopg  5360  brprcneu  5632  funfveu  5652  tz6.12f  5668  funbrfv  5682  ssimaexg  5708  fvmptss2  5721  fvmptssdm  5731  fvmptf  5739  fvelrn  5778  f1veqaeq  5909  dff13f  5910  isopolem  5962  isosolem  5964  riota5f  5997  imbrov2fvoveq  6042  oprabid  6049  ovmpos  6144  ov2gf  6145  ovi3  6158  caovcan  6186  caovordig  6187  caofrss  6266  caoftrn  6267  dfoprab4f  6355  f1o2ndf1  6392  poxp  6396  smoel  6465  tfrlem1  6473  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  nnsucelsuc  6658  nnsucsssuc  6659  nnmordi  6683  nnaordex  6695  qsel  6780  eroveu  6794  ecopovtrn  6800  ecopovtrng  6803  th3qlem2  6806  ixpsnf1o  6904  fundmeng  6981  modom  6993  phplem3g  7041  nneneq  7042  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  findcard  7076  findcard2  7077  findcard2s  7078  findcard2d  7079  findcard2sd  7080  diffifi  7082  ac6sfi  7086  fiintim  7122  fisseneq  7126  fidcenumlemrk  7152  fidcenumlemr  7153  isbth  7165  supeq3  7188  supeq123d  7189  supmoti  7191  suplubti  7198  supisolem  7206  cnvinfex  7216  eqinfti  7218  infvalti  7220  ordiso2  7233  nninfninc  7321  nnnninfeq2  7327  isomni  7334  finomni  7338  exmidomni  7340  ctssexmid  7348  ismkv  7351  ismkvnex  7353  mkvprop  7356  fodjumkvlemres  7357  enmkvlem  7359  iswomni  7363  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  tapeq1  7470  exmidapne  7478  ccfunen  7482  ltsonq  7617  ltexnqq  7627  prcdnql  7703  prcunqu  7704  prloc  7710  prdisj  7711  genprndl  7740  genprndu  7741  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemcl  7895  caucvgprprlemcbv  7906  caucvgprprlemval  7907  suplocexprlemloc  7940  lttrsr  7981  ltsosr  7983  recexgt0sr  7992  mulgt0sr  7997  aptisr  7998  mulextsr1  8000  srpospr  8002  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  caucvgsr  8021  map2psrprg  8024  suplocsrlemb  8025  axprecex  8099  axpre-ltwlin  8102  axpre-lttrn  8103  axpre-apti  8104  axpre-mulgt0  8106  axpre-mulext  8107  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  axsuploc  8251  ltleletr  8260  ltordlem  8661  squeeze0  9083  sup3exmid  9136  nnsub  9181  fzind  9594  uzind4s  9823  uzind4s2  9824  indstr  9826  supinfneg  9828  infsupneg  9829  frec2uzuzd  10663  frec2uzltd  10664  uzsinds  10705  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  seqf1oglem2  10781  seqf1og  10782  seq3id2  10787  seqhomog  10791  expcl2lemap  10812  nn0ltexp2  10970  facdiv  10999  facwordi  11001  zfz1isolem1  11103  zfz1iso  11104  seq3coll  11105  wrdind  11302  wrd2ind  11303  swrdccatin1  11305  swrdccat3blem  11319  reuccatpfxs1lem  11326  caucvgre  11541  fimaxre2  11787  climcn1  11868  climcn2  11869  subcn2  11871  summodclem2a  11941  fsumsplitf  11968  fsum2d  11995  modfsummod  12018  fsumabs  12025  telfsumo  12026  fsumiun  12037  prodfdivap  12107  fprod2d  12183  fproddivapf  12191  fprodsplitf  12192  fprodsplit1f  12194  ndvdssub  12490  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemzz  12572  bezoutlemsup  12579  dfgcd2  12584  algcvg  12619  algcvga  12622  algfx  12623  lcmgcdlem  12648  lcmdvds  12650  coprmgcdb  12659  coprmdvds1  12662  coprmdvds2  12664  prmind2  12691  dvdsprime  12693  nprm  12694  dvdsprm  12708  exprmfct  12709  isprm5lem  12712  coprm  12715  isprm6  12718  prmfac1  12723  sqrt2irr  12733  pcqmul  12875  pcqcl  12878  pc2dvds  12902  pcz  12904  prmpwdvds  12927  ennnfonelemim  13044  exmidunben  13046  infpn2  13076  setscomd  13122  mhmlem  13700  isnsg2  13789  ghmf1  13859  islring  14205  lringuplu  14209  rrgval  14275  rrgeq0i  14277  isdomn  14282  domneq0  14285  opprdomnbg  14287  znidom  14670  znrrg  14673  mplvalcoe  14703  mplsubgfilemcl  14712  uniopn  14724  fiinopn  14727  epttop  14813  cnpval  14921  iscnp  14922  icnpimaex  14934  lmcvg  14940  cnptoprest  14962  cnptoprest2  14963  lmss  14969  lmff  14972  txcnp  14994  txlm  15002  cnmpt12  15010  cnmpt22  15017  blssps  15150  blss  15151  metss  15217  comet  15222  metcnp3  15234  metcnp2  15236  txmetcnp  15241  divcnap  15288  mpomulcn  15289  elcncf2  15297  cncfi  15301  mulc1cncf  15312  cncfmet  15315  mulcncflem  15330  mulcncf  15331  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeulemeu  15345  suplociccreex  15347  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemeu  15354  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthreinc  15368  limccl  15382  ellimc3apf  15383  limccnpcntop  15398  limccnp2lem  15399  limccoap  15401  dvcoapbr  15430  dvmptfsum  15448  mpodvdsmulf1o  15713  perfectlem2  15723  lgsdir2lem4  15759  gausslemma2dlem0i  15785  lgseisenlem2  15799  lgsquad2lem2  15810  2sqlem6  15848  2sqlem8  15851  2sqlem10  15853  gropd  15897  grstructd2dom  15898  upgredg2vtx  15998  upgredgpr  15999  cbvrald  16384  bj-bdfindes  16544  bj-omtrans  16551  bj-inf2vnlem1  16565  bj-inf2vnlem2  16566  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  bj-findes  16576  strcoll2  16578  sscoll2  16583  subctctexmid  16601  pw1nct  16604  exmidsbthrlem  16626  sbthom  16630  apdiff  16652  ismkvnnlem  16656  nconstwlpolem  16669  neapmkv  16672  neap0mkv  16673  ltlenmkv  16674