Theorem imbi12d 223

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
imbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
imbi12d	⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi1d 220	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 219	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 177	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfbidf  1432  drnf1  1621  drnf2  1622  equveli  1642  ax11v2  1701  ax11v  1708  ax11ev  1709  equs5or  1711  mobidh  1934  mobid  1935  axext3  2023  cbvralf  2527  cbvraldva2  2537  gencbval  2602  vtoclgaf  2618  vtocl2gaf  2620  vtocl3gaf  2622  rspct  2649  rspc  2650  ceqex  2671  ralab2  2705  mob2  2721  mob  2723  morex  2725  reu7  2736  reu8  2737  nelrdva  2746  cdeqim  2757  sbcimg  2804  csbhypf  2885  cbvralcsf  2908  dfss2f  2936  sbcssg  3330  sneqrg  3533  elintab  3626  intss1  3630  intmin  3635  dfiin2g  3690  trel  3861  trss  3863  bnd2  3926  zfpow  3928  rext  3951  opth  3974  copsexg  3981  poeq1  4036  pocl  4040  swopolem  4042  swopo  4043  soeq1  4052  sowlin  4057  frforeq2  4082  frforeq3  4084  frirrg  4087  frind  4089  weeq1  4093  ordelord  4118  reusv3i  4191  ordtriexmid  4247  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  ordsucunielexmid  4256  regexmidlem1  4258  regexmid  4260  reg2exmid  4261  elirr  4266  en2lp  4278  ordsoexmid  4286  onintexmid  4297  reg3exmid  4304  tfis  4306  tfisi  4310  peano2  4318  findes  4326  nnregexmid  4342  vtoclr  4388  poinxp  4409  soinxp  4410  posng  4412  ssrel  4428  ssrel2  4430  ssrelrel  4440  relop  4486  issref  4707  iota5  4887  dffun4f  4918  sbcfung  4925  funopg  4934  brprcneu  5171  funfveu  5188  tz6.12f  5202  funbrfv  5212  ssimaexg  5235  fvmptss2  5247  fvmptssdm  5255  fvmptf  5263  fvelrn  5298  f1veqaeq  5408  dff13f  5409  isopolem  5461  isosolem  5463  riota5f  5492  oprabid  5537  ovmpt2s  5624  ov2gf  5625  ovi3  5637  caovcan  5665  caovordig  5666  caofrss  5735  caoftrn  5736  dfoprab4f  5819  f1o2ndf1  5849  poxp  5853  smoel  5915  tfrlem1  5923  nnsucelsuc  6070  nnsucsssuc  6071  nnmordi  6089  nnaordex  6100  qsel  6183  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem2  6209  fundmeng  6287  phplem3g  6319  nneneq  6320  ssfiexmid  6336  findcard  6345  findcard2  6346  findcard2s  6347  findcard2d  6348  findcard2sd  6349  diffifi  6351  ac6sfi  6352  ordiso2  6357  ltsonq  6496  ltexnqq  6506  prcdnql  6582  prcunqu  6583  prloc  6589  prdisj  6590  genprndl  6619  genprndu  6620  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemcl  6774  caucvgprprlemcbv  6785  caucvgprprlemval  6786  lttrsr  6847  ltsosr  6849  recexgt0sr  6858  mulgt0sr  6862  aptisr  6863  mulextsr1  6865  srpospr  6867  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  caucvgsr  6886  axprecex  6954  axpre-ltwlin  6957  axpre-lttrn  6958  axpre-apti  6959  axpre-mulgt0  6961  axpre-mulext  6962  axcaucvglemcau  6972  axcaucvglemres  6973  ltleletr  7100  squeeze0  7870  nnsub  7952  fzind  8353  uzind4s  8533  uzind4s2  8534  indstr  8536  frec2uzzd  9186  frec2uzuzd  9188  frec2uzltd  9189  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  expcl2lemap  9267  caucvgre  9580  climcn1  9829  climcn2  9830  subcn2  9832  sqrt2irr  9878  ialgcvg  9887  ialgcvga  9890  ialgfx  9891  cbvrald  9927  bj-bdfindes  10074  bj-omtrans  10081  bj-inf2vnlem1  10095  bj-inf2vnlem2  10096  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098  bj-findes  10106  strcoll2  10108  sscoll2  10113