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  840  nfbidf  1588  drnf1  1781  drnf2  1782  equveli  1807  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  mobidh  2113  mobid  2114  axext3  2214  cbvralfw  2757  cbvralf  2759  cbvralvw  2772  cbvraldva2  2775  gencbval  2853  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  rspct  2904  rspc  2905  rspc2gv  2923  ceqex  2934  ralab2  2971  mob2  2987  mob  2989  morex  2991  reu7  3002  reu8  3003  nelrdva  3014  cdeqim  3025  sbcimg  3074  csbhypf  3167  cbvralcsf  3191  dfss2f  3219  sbcssg  3605  sneqrg  3850  elintab  3944  intss1  3948  intmin  3953  dfiin2g  4008  disji2  4085  disjiun  4088  trel  4199  trss  4201  bnd2  4269  zfpow  4271  exmidexmid  4292  exmidsssnc  4299  exmidundifim  4303  exmid1stab  4304  rext  4313  opth  4335  copsexg  4342  poeq1  4402  pocl  4406  swopolem  4408  swopo  4409  soeq1  4418  sowlin  4423  frforeq2  4448  frforeq3  4450  frirrg  4453  frind  4455  weeq1  4459  ordelord  4484  reusv3i  4562  ordtriexmid  4625  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  ordsucunielexmid  4635  regexmidlem1  4637  regexmid  4639  reg2exmid  4640  elirr  4645  en2lp  4658  ordsoexmid  4666  onintexmid  4677  reg3exmid  4684  tfis  4687  tfisi  4691  peano2  4699  findes  4707  nnregexmid  4725  omsinds  4726  vtoclr  4780  poinxp  4801  soinxp  4802  posng  4804  ssrel  4820  ssrel2  4822  ssrelrel  4832  relop  4886  issref  5126  iotaexab  5312  iota5  5315  dffun4f  5349  sbcfung  5357  funopg  5367  brprcneu  5641  funfveu  5661  tz6.12f  5677  funbrfv  5691  ssimaexg  5717  fvmptss2  5730  fvmptssdm  5740  fvmptf  5748  fvelrn  5786  f1veqaeq  5920  dff13f  5921  isopolem  5973  isosolem  5975  riota5f  6008  imbrov2fvoveq  6053  oprabid  6060  ovmpos  6155  ov2gf  6156  ovi3  6169  caovcan  6197  caovordig  6198  caofrss  6276  caoftrn  6277  dfoprab4f  6365  f1o2ndf1  6402  poxp  6406  suppfnss  6435  smoel  6509  tfrlem1  6517  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  nnsucelsuc  6702  nnsucsssuc  6703  nnmordi  6727  nnaordex  6739  qsel  6824  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem2  6850  ixpsnf1o  6948  fundmeng  7025  modom  7037  phplem3g  7085  nneneq  7086  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard  7120  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  diffifi  7126  ac6sfi  7130  fiintim  7166  fisseneq  7170  fidcenumlemrk  7196  fidcenumlemr  7197  isbth  7209  supeq3  7232  supeq123d  7233  supmoti  7235  suplubti  7242  supisolem  7250  cnvinfex  7260  eqinfti  7262  infvalti  7264  ordiso2  7277  nninfninc  7365  nnnninfeq2  7371  isomni  7378  finomni  7382  exmidomni  7384  ctssexmid  7392  ismkv  7395  ismkvnex  7397  mkvprop  7400  fodjumkvlemres  7401  enmkvlem  7403  iswomni  7407  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  tapeq1  7514  exmidapne  7522  ccfunen  7526  ltsonq  7661  ltexnqq  7671  prcdnql  7747  prcunqu  7748  prloc  7754  prdisj  7755  genprndl  7784  genprndu  7785  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemcl  7939  caucvgprprlemcbv  7950  caucvgprprlemval  7951  suplocexprlemloc  7984  lttrsr  8025  ltsosr  8027  recexgt0sr  8036  mulgt0sr  8041  aptisr  8042  mulextsr1  8044  srpospr  8046  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  caucvgsr  8065  map2psrprg  8068  suplocsrlemb  8069  axprecex  8143  axpre-ltwlin  8146  axpre-lttrn  8147  axpre-apti  8148  axpre-mulgt0  8150  axpre-mulext  8151  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  axsuploc  8294  ltleletr  8303  ltordlem  8704  squeeze0  9126  sup3exmid  9179  nnsub  9224  fzind  9639  uzind4s  9868  uzind4s2  9869  indstr  9871  supinfneg  9873  infsupneg  9874  frec2uzuzd  10710  frec2uzltd  10711  uzsinds  10752  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord  10793  seq3split  10796  seqsplitg  10797  seqf1oglem2  10828  seqf1og  10829  seq3id2  10834  seqhomog  10838  expcl2lemap  10859  nn0ltexp2  11017  facdiv  11046  facwordi  11048  zfz1isolem1  11150  zfz1iso  11151  seq3coll  11152  wrdind  11352  wrd2ind  11353  swrdccatin1  11355  swrdccat3blem  11369  reuccatpfxs1lem  11376  caucvgre  11604  fimaxre2  11850  climcn1  11931  climcn2  11932  subcn2  11934  summodclem2a  12005  fsumsplitf  12032  fsum2d  12059  modfsummod  12082  fsumabs  12089  telfsumo  12090  fsumiun  12101  prodfdivap  12171  fprod2d  12247  fproddivapf  12255  fprodsplitf  12256  fprodsplit1f  12258  ndvdssub  12554  bezoutlemmain  12632  bezoutlemex  12635  bezoutlemzz  12636  bezoutlemsup  12643  dfgcd2  12648  algcvg  12683  algcvga  12686  algfx  12687  lcmgcdlem  12712  lcmdvds  12714  coprmgcdb  12723  coprmdvds1  12726  coprmdvds2  12728  prmind2  12755  dvdsprime  12757  nprm  12758  dvdsprm  12772  exprmfct  12773  isprm5lem  12776  coprm  12779  isprm6  12782  prmfac1  12787  sqrt2irr  12797  pcqmul  12939  pcqcl  12942  pc2dvds  12966  pcz  12968  prmpwdvds  12991  ennnfonelemim  13108  exmidunben  13110  infpn2  13140  setscomd  13186  mhmlem  13764  isnsg2  13853  ghmf1  13923  islring  14270  lringuplu  14274  rrgval  14340  rrgeq0i  14342  isdomn  14348  domneq0  14351  opprdomnbg  14353  znidom  14736  znrrg  14739  mplvalcoe  14774  mplsubgfilemcl  14783  uniopn  14795  fiinopn  14798  epttop  14884  cnpval  14992  iscnp  14993  icnpimaex  15005  lmcvg  15011  cnptoprest  15033  cnptoprest2  15034  lmss  15040  lmff  15043  txcnp  15065  txlm  15073  cnmpt12  15081  cnmpt22  15088  blssps  15221  blss  15222  metss  15288  comet  15293  metcnp3  15305  metcnp2  15307  txmetcnp  15312  divcnap  15359  mpomulcn  15360  elcncf2  15368  cncfi  15372  mulc1cncf  15383  cncfmet  15386  mulcncflem  15401  mulcncf  15402  dedekindeulemloc  15413  dedekindeulemlu  15415  dedekindeulemeu  15416  suplociccreex  15418  dedekindicclemloc  15422  dedekindicclemlu  15424  dedekindicclemeu  15425  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemloc  15435  ivthreinc  15439  limccl  15453  ellimc3apf  15454  limccnpcntop  15469  limccnp2lem  15470  limccoap  15472  dvcoapbr  15501  dvmptfsum  15519  mpodvdsmulf1o  15787  perfectlem2  15797  lgsdir2lem4  15833  gausslemma2dlem0i  15859  lgseisenlem2  15873  lgsquad2lem2  15884  2sqlem6  15922  2sqlem8  15925  2sqlem10  15927  gropd  15971  grstructd2dom  15972  upgredg2vtx  16072  upgredgpr  16073  eupth2fi  16403  cbvrald  16489  bj-bdfindes  16648  bj-omtrans  16655  bj-inf2vnlem1  16669  bj-inf2vnlem2  16670  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  bj-findes  16680  strcoll2  16682  sscoll2  16687  subctctexmid  16705  pw1nct  16708  exmidnotnotr  16710  exmidcon  16711  exmidsbthrlem  16733  sbthom  16737  apdiff  16763  ismkvnnlem  16768  nconstwlpolem  16781  neapmkv  16784  neap0mkv  16785  ltlenmkv  16786