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  834  nfbidf  1562  drnf1  1756  drnf2  1757  equveli  1782  ax11v2  1843  ax11v  1850  ax11ev  1851  equs5or  1853  mobidh  2088  mobid  2089  axext3  2188  cbvralfw  2728  cbvralf  2730  cbvralvw  2742  cbvraldva2  2745  gencbval  2821  vtoclgaf  2838  vtocl2gaf  2840  vtocl3gaf  2842  rspct  2870  rspc  2871  rspc2gv  2889  ceqex  2900  ralab2  2937  mob2  2953  mob  2955  morex  2957  reu7  2968  reu8  2969  nelrdva  2980  cdeqim  2991  sbcimg  3040  csbhypf  3132  cbvralcsf  3156  dfss2f  3184  sbcssg  3569  sneqrg  3803  elintab  3896  intss1  3900  intmin  3905  dfiin2g  3960  disji2  4037  disjiun  4039  trel  4149  trss  4151  bnd2  4217  zfpow  4219  exmidexmid  4240  exmidsssnc  4247  exmidundifim  4251  exmid1stab  4252  rext  4259  opth  4281  copsexg  4288  poeq1  4346  pocl  4350  swopolem  4352  swopo  4353  soeq1  4362  sowlin  4367  frforeq2  4392  frforeq3  4394  frirrg  4397  frind  4399  weeq1  4403  ordelord  4428  reusv3i  4506  ordtriexmid  4569  ontr2exmid  4573  onsucsssucexmid  4575  onsucelsucexmid  4578  ordsucunielexmid  4579  regexmidlem1  4581  regexmid  4583  reg2exmid  4584  elirr  4589  en2lp  4602  ordsoexmid  4610  onintexmid  4621  reg3exmid  4628  tfis  4631  tfisi  4635  peano2  4643  findes  4651  nnregexmid  4669  omsinds  4670  vtoclr  4723  poinxp  4744  soinxp  4745  posng  4747  ssrel  4763  ssrel2  4765  ssrelrel  4775  relop  4828  issref  5065  iotaexab  5250  iota5  5253  dffun4f  5287  sbcfung  5295  funopg  5305  brprcneu  5569  funfveu  5589  tz6.12f  5605  funbrfv  5617  ssimaexg  5641  fvmptss2  5654  fvmptssdm  5664  fvmptf  5672  fvelrn  5711  f1veqaeq  5838  dff13f  5839  isopolem  5891  isosolem  5893  riota5f  5924  imbrov2fvoveq  5969  oprabid  5976  ovmpos  6069  ov2gf  6070  ovi3  6083  caovcan  6111  caovordig  6112  caofrss  6190  caoftrn  6191  dfoprab4f  6279  f1o2ndf1  6314  poxp  6318  smoel  6386  tfrlem1  6394  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemaccex  6434  tfr1onlemres  6435  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  tfrcllemres  6448  tfrcl  6450  nnsucelsuc  6577  nnsucsssuc  6578  nnmordi  6602  nnaordex  6614  qsel  6699  eroveu  6713  ecopovtrn  6719  ecopovtrng  6722  th3qlem2  6725  ixpsnf1o  6823  fundmeng  6899  phplem3g  6953  nneneq  6954  ssfiexmid  6973  domfiexmid  6975  findcard  6985  findcard2  6986  findcard2s  6987  findcard2d  6988  findcard2sd  6989  diffifi  6991  ac6sfi  6995  fiintim  7028  fisseneq  7031  fidcenumlemrk  7056  fidcenumlemr  7057  isbth  7069  supeq3  7092  supeq123d  7093  supmoti  7095  suplubti  7102  supisolem  7110  cnvinfex  7120  eqinfti  7122  infvalti  7124  ordiso2  7137  nninfninc  7225  nnnninfeq2  7231  isomni  7238  finomni  7242  exmidomni  7244  ctssexmid  7252  ismkv  7255  ismkvnex  7257  mkvprop  7260  fodjumkvlemres  7261  enmkvlem  7263  iswomni  7267  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  tapeq1  7364  exmidapne  7372  ccfunen  7376  ltsonq  7511  ltexnqq  7521  prcdnql  7597  prcunqu  7598  prloc  7604  prdisj  7605  genprndl  7634  genprndu  7635  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemcl  7789  caucvgprprlemcbv  7800  caucvgprprlemval  7801  suplocexprlemloc  7834  lttrsr  7875  ltsosr  7877  recexgt0sr  7886  mulgt0sr  7891  aptisr  7892  mulextsr1  7894  srpospr  7896  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  caucvgsr  7915  map2psrprg  7918  suplocsrlemb  7919  axprecex  7993  axpre-ltwlin  7996  axpre-lttrn  7997  axpre-apti  7998  axpre-mulgt0  8000  axpre-mulext  8001  axcaucvglemcau  8011  axcaucvglemres  8012  axpre-suploclemres  8014  axpre-suploc  8015  axsuploc  8145  ltleletr  8154  ltordlem  8555  squeeze0  8977  sup3exmid  9030  nnsub  9075  fzind  9488  uzind4s  9711  uzind4s2  9712  indstr  9714  supinfneg  9716  infsupneg  9717  frec2uzuzd  10547  frec2uzltd  10548  uzsinds  10589  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  seq3split  10633  seqsplitg  10634  seqf1oglem2  10665  seqf1og  10666  seq3id2  10671  seqhomog  10675  expcl2lemap  10696  nn0ltexp2  10854  facdiv  10883  facwordi  10885  zfz1isolem1  10985  zfz1iso  10986  seq3coll  10987  caucvgre  11292  fimaxre2  11538  climcn1  11619  climcn2  11620  subcn2  11622  summodclem2a  11692  fsumsplitf  11719  fsum2d  11746  modfsummod  11769  fsumabs  11776  telfsumo  11777  fsumiun  11788  prodfdivap  11858  fprod2d  11934  fproddivapf  11942  fprodsplitf  11943  fprodsplit1f  11945  ndvdssub  12241  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemzz  12323  bezoutlemsup  12330  dfgcd2  12335  algcvg  12370  algcvga  12373  algfx  12374  lcmgcdlem  12399  lcmdvds  12401  coprmgcdb  12410  coprmdvds1  12413  coprmdvds2  12415  prmind2  12442  dvdsprime  12444  nprm  12445  dvdsprm  12459  exprmfct  12460  isprm5lem  12463  coprm  12466  isprm6  12469  prmfac1  12474  sqrt2irr  12484  pcqmul  12626  pcqcl  12629  pc2dvds  12653  pcz  12655  prmpwdvds  12678  ennnfonelemim  12795  exmidunben  12797  infpn2  12827  setscomd  12873  mhmlem  13450  isnsg2  13539  ghmf1  13609  islring  13954  lringuplu  13958  rrgval  14024  rrgeq0i  14026  isdomn  14031  domneq0  14034  opprdomnbg  14036  znidom  14419  znrrg  14422  mplvalcoe  14452  mplsubgfilemcl  14461  uniopn  14473  fiinopn  14476  epttop  14562  cnpval  14670  iscnp  14671  icnpimaex  14683  lmcvg  14689  cnptoprest  14711  cnptoprest2  14712  lmss  14718  lmff  14721  txcnp  14743  txlm  14751  cnmpt12  14759  cnmpt22  14766  blssps  14899  blss  14900  metss  14966  comet  14971  metcnp3  14983  metcnp2  14985  txmetcnp  14990  divcnap  15037  mpomulcn  15038  elcncf2  15046  cncfi  15050  mulc1cncf  15061  cncfmet  15064  mulcncflem  15079  mulcncf  15080  dedekindeulemloc  15091  dedekindeulemlu  15093  dedekindeulemeu  15094  suplociccreex  15096  dedekindicclemloc  15100  dedekindicclemlu  15102  dedekindicclemeu  15103  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  ivthreinc  15117  limccl  15131  ellimc3apf  15132  limccnpcntop  15147  limccnp2lem  15148  limccoap  15150  dvcoapbr  15179  dvmptfsum  15197  mpodvdsmulf1o  15462  perfectlem2  15472  lgsdir2lem4  15508  gausslemma2dlem0i  15534  lgseisenlem2  15548  lgsquad2lem2  15559  2sqlem6  15597  2sqlem8  15600  2sqlem10  15602  gropd  15644  grstructd2dom  15645  cbvrald  15724  bj-bdfindes  15885  bj-omtrans  15892  bj-inf2vnlem1  15906  bj-inf2vnlem2  15907  bj-inf2vnlem3  15908  bj-inf2vnlem4  15909  bj-findes  15917  strcoll2  15919  sscoll2  15924  subctctexmid  15937  pw1nct  15940  exmidsbthrlem  15961  sbthom  15965  apdiff  15987  ismkvnnlem  15991  nconstwlpolem  16004  neapmkv  16007  neap0mkv  16008  ltlenmkv  16009