Theorem imbi12d 474

Description: Deduction joining two equivalences to form equivalence of implications.

Hypotheses

Ref	Expression
bi2d.1	⊢ (φ → (ψ ↔ χ))
bi2d.2	⊢ (φ → (θ ↔ τ))

Assertion

Ref	Expression
imbi12d	⊢ (φ → ((ψ → θ) ↔ (χ → τ)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		bi2d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	imbi1d 465	. 2 ⊢ (φ → ((ψ → θ) ↔ (χ → θ)))
3		bi2d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	imbi2d 464	. 2 ⊢ (φ → ((χ → θ) ↔ (χ → τ)))
5	2, 4	bitrd 406	1 ⊢ (φ → ((ψ → θ) ↔ (χ → τ)))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  hbsb4t 906  bimod 1030  axpow 1082  axinf 1084  zfext2 1087  hblem 1170  ralcom2 1314  cbvralf 1330  vtoclga 1387  rcla4v 1402  ceqex 1410  sbcim 1460  dfss2f 1499  rext 1862  copsexg 1902  reuuni2 1956  elinti 1974  elintab 1976  intss1 1979  intmin 1982  ssiun2s 2020  trel 2048  trss 2050  ssopab2 2119  poeq1 2130  pocl 2132  so 2152  supmo 2156  suplub 2161  fri 2170  frc 2172  efrirr 2180  ordelord 2221  tfis 2245  limsuc 2361  dfom2 2374  limomss 2378  nnlim 2385  findsg 2398  findes 2400  tfindsg 2402  tfindsg2 2403  tfindes 2404  vtoclr 2449  ralxp 2456  fneu 2728  tz6.12f 2844  tz6.12i 2847  funbrfv 2852  funopfvg 2854  fnfvbr 2855  fvelima 2859  fvrn 2888  f1fvf 2917  f1fveq 2918  isofrlem 2939  f1oweOLD 2944  tfrlem1 2949  rdglimt 2986  tz7.48lem 2993  tz7.49 2997  caoprcan 3069  oawordeu 3157  omordi 3164  omsmolem 3195  ersym 3209  ertr 3211  ecopoprtrn 3247  th3qlem2 3251  ensymg 3316  sbth 3359  limensuc 3402  nneneq 3408  php 3409  php2 3410  pssnn 3428  fiint 3445  zfregcl 3446  inf0 3457  inf3lem1 3464  inf4 3473  dfom3 3477  elom3 3478  setind 3492  r1ord 3499  rankun 3535  bnd2 3549  aceq3lem 3555  aceq5lem4 3561  aceq5 3563  aceq6b 3565  kmlem1 3580  kmlem4 3583  kmlem9 3588  kmlem11 3590  kmlem12 3591  numthlem 3598  zornlem7 3609  fodomg 3614  unxpdom 3650  sucxpdom 3652  alephordi 3679  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  zfcndpow 3762  zfcndinf 3764  indpi 3828  ltsopq 3869  ltexpq 3874  prcdpq 3891  prnmax 3893  ltsopr 3930  prlem934a 3931  ltsosr 3997  recexsrlem 4006  mulgt0sr 4008  map2psrpr 4014  suppsrlem 4015  suppsr 4016  suppsr2 4017  supsrlem6 4024  supre 4054  ltsor 4055  axrecex 4079  axrrecex 4081  axmulgt0 4086  mulcant2 4209  divmult 4220  divclt 4223  divcan1t 4228  divcan2t 4229  recidt 4235  divrect 4238  divdistrt 4246  divcan3t 4251  redivclt 4276  gt0ne0t 4346  lt2addt 4361  addge0t 4362  mulge0t 4375  ltsqt 4376  recgt0t 4401  divgt0t 4402  divge0t 4403  ltdivt 4404  ltmuldivt 4406  ltrect 4417  lerect 4418  ltdiv23t 4419  le2sqt 4420  peano5nn 4424  peano2nn 4433  nnleltp1t 4448  nnsub 4450  nnunb 4520  crut 4531  uzind 4603  nnwof 4609  zmax 4618  zbtwnre 4619  om2uzlt 4654  sqe11t 4705  lt2sqet 4706  sqrlem6 4736  sqrlem12 4742  sqrclt 4767  sqrgt0t 4768  sqrge0t 4769  sqr00t 4770  sqsqrt 4776  sqr2irrlem2 4778  sqr2irrlem3 4779  absidt 4862  abs3lemt 4865  climunii 4883  ruclem25 4909  ruclem32 4916  normpytht 5092  norm3lemt 5097  closedsub 5128  chlim 5139  hlimcaui 5141  hlimunii 5143  ch2 5149  chcompl 5150  occllem6 5185  occllem8 5187  projlem1 5193  projlem20 5212  projlem28 5220  projlem29 5221  omlsi 5250  h1de2 5458  elspansn2t 5472  h1datomt 5484  pjoml3t 5517  spansncvt 5543  pjcjt2 5580  pjssge0t 5636  pjopytht 5662  stjt 5676  str 5698  stcltr1 5707  mdbr 5726  mdi 5727  mdbr3 5729  mdbr4 5730  dmdbr 5731  dmdi 5732  atss 5744  atom1d 5750  chcv1t 5751  atcvat2t 5773

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org