Theorem imbi12d 233

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 230	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 229	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  818  nfbidf  1519  drnf1  1713  drnf2  1714  equveli  1739  ax11v2  1800  ax11v  1807  ax11ev  1808  equs5or  1810  mobidh  2040  mobid  2041  axext3  2140  cbvralf  2674  cbvralvw  2684  cbvraldva2  2687  gencbval  2760  vtoclgaf  2777  vtocl2gaf  2779  vtocl3gaf  2781  rspct  2809  rspc  2810  rspc2gv  2828  ceqex  2839  ralab2  2876  mob2  2892  mob  2894  morex  2896  reu7  2907  reu8  2908  nelrdva  2919  cdeqim  2930  sbcimg  2978  csbhypf  3069  cbvralcsf  3093  dfss2f  3119  sbcssg  3503  sneqrg  3725  elintab  3818  intss1  3822  intmin  3827  dfiin2g  3882  disji2  3958  disjiun  3960  trel  4069  trss  4071  bnd2  4134  zfpow  4136  exmidexmid  4157  exmidsssnc  4164  exmidundifim  4168  rext  4175  opth  4197  copsexg  4204  poeq1  4259  pocl  4263  swopolem  4265  swopo  4266  soeq1  4275  sowlin  4280  frforeq2  4305  frforeq3  4307  frirrg  4310  frind  4312  weeq1  4316  ordelord  4341  reusv3i  4418  ordtriexmid  4479  ontr2exmid  4483  onsucsssucexmid  4485  onsucelsucexmid  4488  ordsucunielexmid  4489  regexmidlem1  4491  regexmid  4493  reg2exmid  4494  elirr  4499  en2lp  4512  ordsoexmid  4520  onintexmid  4531  reg3exmid  4538  tfis  4541  tfisi  4545  peano2  4553  findes  4561  nnregexmid  4579  omsinds  4580  vtoclr  4633  poinxp  4654  soinxp  4655  posng  4657  ssrel  4673  ssrel2  4675  ssrelrel  4685  relop  4735  issref  4967  iota5  5154  dffun4f  5185  sbcfung  5193  funopg  5203  brprcneu  5460  funfveu  5480  tz6.12f  5496  funbrfv  5506  ssimaexg  5529  fvmptss2  5542  fvmptssdm  5551  fvmptf  5559  fvelrn  5597  f1veqaeq  5716  dff13f  5717  isopolem  5769  isosolem  5771  riota5f  5801  imbrov2fvoveq  5846  oprabid  5850  ovmpos  5941  ov2gf  5942  ovi3  5954  caovcan  5982  caovordig  5983  caofrss  6053  caoftrn  6054  dfoprab4f  6138  f1o2ndf1  6172  poxp  6176  smoel  6244  tfrlem1  6252  tfr1onlemsucfn  6284  tfr1onlemsucaccv  6285  tfr1onlembxssdm  6287  tfr1onlembfn  6288  tfr1onlemaccex  6292  tfr1onlemres  6293  tfrcllemsucfn  6297  tfrcllemsucaccv  6298  tfrcllembxssdm  6300  tfrcllembfn  6301  tfrcllemaccex  6305  tfrcllemres  6306  tfrcl  6308  nnsucelsuc  6435  nnsucsssuc  6436  nnmordi  6460  nnaordex  6471  qsel  6554  eroveu  6568  ecopovtrn  6574  ecopovtrng  6577  th3qlem2  6580  ixpsnf1o  6678  fundmeng  6749  phplem3g  6798  nneneq  6799  ssfiexmid  6818  domfiexmid  6820  findcard  6830  findcard2  6831  findcard2s  6832  findcard2d  6833  findcard2sd  6834  diffifi  6836  ac6sfi  6840  fiintim  6870  fisseneq  6873  fidcenumlemrk  6895  fidcenumlemr  6896  isbth  6908  supeq3  6930  supeq123d  6931  supmoti  6933  suplubti  6940  supisolem  6948  cnvinfex  6958  eqinfti  6960  infvalti  6962  ordiso2  6973  nnnninfeq2  7066  isomni  7073  finomni  7077  exmidomni  7079  ctssexmid  7087  ismkv  7090  ismkvnex  7092  mkvprop  7095  fodjumkvlemres  7096  enmkvlem  7098  iswomni  7102  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  ccfunen  7178  ltsonq  7312  ltexnqq  7322  prcdnql  7398  prcunqu  7399  prloc  7405  prdisj  7406  genprndl  7435  genprndu  7436  caucvgprlemnkj  7580  caucvgprlemnbj  7581  caucvgprlemcl  7590  caucvgprprlemcbv  7601  caucvgprprlemval  7602  suplocexprlemloc  7635  lttrsr  7676  ltsosr  7678  recexgt0sr  7687  mulgt0sr  7692  aptisr  7693  mulextsr1  7695  srpospr  7697  caucvgsrlemgt1  7709  caucvgsrlemoffres  7714  caucvgsr  7716  map2psrprg  7719  suplocsrlemb  7720  axprecex  7794  axpre-ltwlin  7797  axpre-lttrn  7798  axpre-apti  7799  axpre-mulgt0  7801  axpre-mulext  7802  axcaucvglemcau  7812  axcaucvglemres  7813  axpre-suploclemres  7815  axpre-suploc  7816  axsuploc  7944  ltleletr  7953  ltordlem  8351  squeeze0  8769  sup3exmid  8822  nnsub  8866  fzind  9273  uzind4s  9495  uzind4s2  9496  indstr  9498  supinfneg  9500  infsupneg  9501  frec2uzuzd  10294  frec2uzltd  10295  uzsinds  10334  seq3fveq2  10361  seq3shft2  10365  monoord  10368  seq3split  10371  seq3id2  10401  expcl2lemap  10424  facdiv  10605  facwordi  10607  zfz1isolem1  10704  zfz1iso  10705  seq3coll  10706  caucvgre  10874  fimaxre2  11119  climcn1  11198  climcn2  11199  subcn2  11201  summodclem2a  11271  fsumsplitf  11298  fsum2d  11325  modfsummod  11348  fsumabs  11355  telfsumo  11356  fsumiun  11367  prodfdivap  11437  fprod2d  11513  fproddivapf  11521  fprodsplitf  11522  fprodsplit1f  11524  ndvdssub  11813  bezoutlemmain  11873  bezoutlemex  11876  bezoutlemzz  11877  bezoutlemsup  11884  dfgcd2  11889  algcvg  11916  algcvga  11919  algfx  11920  lcmgcdlem  11945  lcmdvds  11947  coprmgcdb  11956  coprmdvds1  11959  coprmdvds2  11961  prmind2  11988  dvdsprime  11990  nprm  11991  dvdsprm  12004  exprmfct  12005  coprm  12009  isprm6  12012  prmfac1  12017  sqrt2irr  12027  ennnfonelemim  12136  exmidunben  12138  uniopn  12370  fiinopn  12373  epttop  12461  cnpval  12569  iscnp  12570  icnpimaex  12582  lmcvg  12588  cnptoprest  12610  cnptoprest2  12611  lmss  12617  lmff  12620  txcnp  12642  txlm  12650  cnmpt12  12658  cnmpt22  12665  blssps  12798  blss  12799  metss  12865  comet  12870  metcnp3  12882  metcnp2  12884  txmetcnp  12889  divcnap  12926  elcncf2  12932  cncfi  12936  mulc1cncf  12947  cncfmet  12950  mulcncflem  12961  mulcncf  12962  dedekindeulemloc  12968  dedekindeulemlu  12970  dedekindeulemeu  12971  suplociccreex  12973  dedekindicclemloc  12977  dedekindicclemlu  12979  dedekindicclemeu  12980  ivthinclemlopn  12985  ivthinclemlr  12986  ivthinclemuopn  12987  ivthinclemur  12988  ivthinclemloc  12990  limccl  12999  ellimc3apf  13000  limccnpcntop  13015  limccnp2lem  13016  limccoap  13018  dvcoapbr  13042  cbvrald  13333  bj-bdfindes  13495  bj-omtrans  13502  bj-inf2vnlem1  13516  bj-inf2vnlem2  13517  bj-inf2vnlem3  13518  bj-inf2vnlem4  13519  bj-findes  13527  strcoll2  13529  sscoll2  13534  exmid1stab  13543  subctctexmid  13544  pw1nct  13546  exmidsbthrlem  13564  sbthom  13568  apdiff  13590  ismkvnnlem  13594  nconstwlpolem  13606  neapmkv  13609