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  1782  drnf2  1783  equveli  1808  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  mobidh  2114  mobid  2115  axext3  2215  cbvralfw  2767  cbvralf  2769  cbvralvw  2782  cbvraldva2  2785  gencbval  2863  vtoclgaf  2880  vtocl2gaf  2882  vtocl3gaf  2884  rspct  2914  rspc  2915  rspc2gv  2933  ceqex  2944  ralab2  2981  mob2  2997  mob  2999  morex  3001  reu7  3012  reu8  3013  nelrdva  3024  cdeqim  3035  sbcimg  3084  csbhypf  3177  cbvralcsf  3201  dfss2f  3229  sbcssg  3618  sneqrg  3866  elintab  3960  intss1  3964  intmin  3969  dfiin2g  4024  disji2  4101  disjiun  4104  trel  4215  trss  4217  bnd2  4286  zfpow  4288  exmidexmid  4309  exmidsssnc  4316  exmidundifim  4320  exmid1stab  4321  rext  4331  opth  4353  copsexg  4360  poeq1  4420  pocl  4424  swopolem  4426  swopo  4427  soeq1  4436  sowlin  4441  frforeq2  4466  frforeq3  4468  frirrg  4471  frind  4473  weeq1  4477  ordelord  4502  reusv3i  4580  ordtriexmid  4643  ontr2exmid  4647  onsucsssucexmid  4649  onsucelsucexmid  4652  ordsucunielexmid  4653  regexmidlem1  4655  regexmid  4657  reg2exmid  4658  elirr  4663  en2lp  4676  ordsoexmid  4684  onintexmid  4695  reg3exmid  4702  tfis  4705  tfisi  4709  peano2  4717  findes  4725  nnregexmid  4743  omsinds  4744  vtoclr  4798  poinxp  4819  soinxp  4820  posng  4822  ssrel  4838  ssrel2  4840  ssrelrel  4850  relop  4905  issref  5145  iotaexab  5331  iota5  5334  dffun4f  5368  sbcfung  5376  funopg  5386  brprcneu  5663  funfveu  5683  tz6.12f  5699  funbrfv  5713  ssimaexg  5739  fvmptss2  5752  fvmptssdm  5762  fvmptf  5770  fvelrn  5808  f1veqaeq  5942  dff13f  5943  isopolem  5995  isosolem  5997  riota5f  6030  imbrov2fvoveq  6075  oprabid  6082  ovmpos  6177  ov2gf  6178  ovi3  6191  caovcan  6219  caovordig  6220  caofrss  6298  caoftrn  6299  dfoprab4f  6387  f1o2ndf1  6424  poxp  6428  suppfnss  6457  smoel  6531  tfrlem1  6539  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemaccex  6592  tfrcllemres  6593  tfrcl  6595  nnsucelsuc  6724  nnsucsssuc  6725  nnmordi  6749  nnaordex  6761  qsel  6846  eroveu  6860  ecopovtrn  6866  ecopovtrng  6869  th3qlem2  6872  ixpsnf1o  6971  fundmeng  7048  modom  7061  phplem3g  7110  nneneq  7111  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  findcard  7145  findcard2  7146  findcard2s  7147  findcard2d  7148  findcard2sd  7149  diffifi  7151  ac6sfi  7155  fiintim  7191  fisseneq  7195  fidcenumlemrk  7224  fidcenumlemr  7225  isbth  7237  supeq3  7281  supeq123d  7282  supmoti  7284  suplubti  7291  supisolem  7299  cnvinfex  7309  eqinfti  7311  infvalti  7313  ordiso2  7326  nninfninc  7414  nnnninfeq2  7420  isomni  7427  finomni  7431  exmidomni  7433  ctssexmid  7441  ismkv  7444  ismkvnex  7446  mkvprop  7449  fodjumkvlemres  7450  enmkvlem  7452  iswomni  7456  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  papsym  7561  papcotr  7562  tapeq1  7566  exmidapne  7574  ccfunen  7578  ltsonq  7713  ltexnqq  7723  prcdnql  7799  prcunqu  7800  prloc  7806  prdisj  7807  genprndl  7836  genprndu  7837  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemcl  7991  caucvgprprlemcbv  8002  caucvgprprlemval  8003  suplocexprlemloc  8036  lttrsr  8077  ltsosr  8079  recexgt0sr  8088  mulgt0sr  8093  aptisr  8094  mulextsr1  8096  srpospr  8098  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  caucvgsr  8117  map2psrprg  8120  suplocsrlemb  8121  axprecex  8195  axpre-ltwlin  8198  axpre-lttrn  8199  axpre-apti  8200  axpre-mulgt0  8202  axpre-mulext  8203  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  axsuploc  8346  ltleletr  8355  ltordlem  8756  squeeze0  9178  sup3exmid  9231  nnsub  9276  fzind  9693  uzind4s  9922  uzind4s2  9923  indstr  9925  supinfneg  9927  infsupneg  9928  frec2uzuzd  10764  frec2uzltd  10765  uzsinds  10806  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  seqf1oglem2  10882  seqf1og  10883  seq3id2  10888  seqhomog  10892  expcl2lemap  10913  nn0ltexp2  11071  facdiv  11100  facwordi  11102  zfz1isolem1  11212  zfz1iso  11213  seq3coll  11214  wrdind  11414  wrd2ind  11415  swrdccatin1  11417  swrdccat3blem  11431  reuccatpfxs1lem  11438  caucvgre  11666  fimaxre2  11912  climcn1  11993  climcn2  11994  subcn2  11996  summodclem2a  12067  fsumsplitf  12094  fsum2d  12121  modfsummod  12144  fsumabs  12151  telfsumo  12152  fsumiun  12163  prodfdivap  12233  fprod2d  12309  fproddivapf  12317  fprodsplitf  12318  fprodsplit1f  12320  ndvdssub  12616  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemzz  12698  bezoutlemsup  12705  dfgcd2  12710  algcvg  12745  algcvga  12748  algfx  12749  lcmgcdlem  12774  lcmdvds  12776  coprmgcdb  12785  coprmdvds1  12788  coprmdvds2  12790  prmind2  12817  dvdsprime  12819  nprm  12820  dvdsprm  12834  exprmfct  12835  isprm5lem  12838  coprm  12841  isprm6  12844  prmfac1  12849  sqrt2irr  12859  pcqmul  13001  pcqcl  13004  pc2dvds  13028  pcz  13030  prmpwdvds  13053  ballotfilem2  13142  ennnfonelemim  13175  exmidunben  13177  infpn2  13207  setscomd  13253  mhmlem  13831  isnsg2  13920  ghmf1  13990  islring  14337  lringuplu  14341  rrgval  14407  rrgeq0i  14409  isdomn  14415  domneq0  14418  opprdomnbg  14420  znidom  14805  znrrg  14808  mplvalcoe  14845  mplsubgfilemcl  14854  uniopn  14866  fiinopn  14869  epttop  14955  cnpval  15063  iscnp  15064  icnpimaex  15076  lmcvg  15082  cnptoprest  15104  cnptoprest2  15105  lmss  15111  lmff  15114  txcnp  15136  txlm  15144  cnmpt12  15152  cnmpt22  15159  blssps  15292  blss  15293  metss  15359  comet  15364  metcnp3  15376  metcnp2  15378  txmetcnp  15383  divcnap  15430  mpomulcn  15431  elcncf2  15439  cncfi  15443  mulc1cncf  15454  cncfmet  15457  mulcncflem  15472  mulcncf  15473  dedekindeulemloc  15484  dedekindeulemlu  15486  dedekindeulemeu  15487  suplociccreex  15489  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicclemeu  15496  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemloc  15506  ivthreinc  15510  limccl  15524  ellimc3apf  15525  limccnpcntop  15540  limccnp2lem  15541  limccoap  15543  dvcoapbr  15572  dvmptfsum  15590  mpodvdsmulf1o  15858  perfectlem2  15868  lgsdir2lem4  15904  gausslemma2dlem0i  15930  lgseisenlem2  15944  lgsquad2lem2  15955  2sqlem6  15993  2sqlem8  15996  2sqlem10  15998  gropd  16042  grstructd2dom  16043  upgredg2vtx  16143  upgredgpr  16144  eupth2fi  16474  cbvrald  16560  bj-bdfindes  16719  bj-omtrans  16726  bj-inf2vnlem1  16740  bj-inf2vnlem2  16741  bj-inf2vnlem3  16742  bj-inf2vnlem4  16743  bj-findes  16751  strcoll2  16753  sscoll2  16758  subctctexmid  16774  pw1nct  16777  exmidnotnotr  16779  exmidcon  16780  exmidsbthrlem  16802  sbthom  16806  apdiff  16832  ismkvnnlem  16837  nconstwlpolem  16851  neapmkv  16854  neap0mkv  16855  ltlenmkv  16856