Theorem imbi12d 234

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

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  837  nfbidf  1585  drnf1  1779  drnf2  1780  equveli  1805  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  mobidh  2111  mobid  2112  axext3  2212  cbvralfw  2754  cbvralf  2756  cbvralvw  2769  cbvraldva2  2772  gencbval  2850  vtoclgaf  2867  vtocl2gaf  2869  vtocl3gaf  2871  rspct  2901  rspc  2902  rspc2gv  2920  ceqex  2931  ralab2  2968  mob2  2984  mob  2986  morex  2988  reu7  2999  reu8  3000  nelrdva  3011  cdeqim  3022  sbcimg  3071  csbhypf  3164  cbvralcsf  3188  dfss2f  3216  sbcssg  3601  sneqrg  3843  elintab  3937  intss1  3941  intmin  3946  dfiin2g  4001  disji2  4078  disjiun  4081  trel  4192  trss  4194  bnd2  4261  zfpow  4263  exmidexmid  4284  exmidsssnc  4291  exmidundifim  4295  exmid1stab  4296  rext  4305  opth  4327  copsexg  4334  poeq1  4394  pocl  4398  swopolem  4400  swopo  4401  soeq1  4410  sowlin  4415  frforeq2  4440  frforeq3  4442  frirrg  4445  frind  4447  weeq1  4451  ordelord  4476  reusv3i  4554  ordtriexmid  4617  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  ordsucunielexmid  4627  regexmidlem1  4629  regexmid  4631  reg2exmid  4632  elirr  4637  en2lp  4650  ordsoexmid  4658  onintexmid  4669  reg3exmid  4676  tfis  4679  tfisi  4683  peano2  4691  findes  4699  nnregexmid  4717  omsinds  4718  vtoclr  4772  poinxp  4793  soinxp  4794  posng  4796  ssrel  4812  ssrel2  4814  ssrelrel  4824  relop  4878  issref  5117  iotaexab  5303  iota5  5306  dffun4f  5340  sbcfung  5348  funopg  5358  brprcneu  5628  funfveu  5648  tz6.12f  5664  funbrfv  5678  ssimaexg  5704  fvmptss2  5717  fvmptssdm  5727  fvmptf  5735  fvelrn  5774  f1veqaeq  5905  dff13f  5906  isopolem  5958  isosolem  5960  riota5f  5993  imbrov2fvoveq  6038  oprabid  6045  ovmpos  6140  ov2gf  6141  ovi3  6154  caovcan  6182  caovordig  6183  caofrss  6262  caoftrn  6263  dfoprab4f  6351  f1o2ndf1  6388  poxp  6392  smoel  6461  tfrlem1  6469  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  nnsucelsuc  6654  nnsucsssuc  6655  nnmordi  6679  nnaordex  6691  qsel  6776  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem2  6802  ixpsnf1o  6900  fundmeng  6977  modom  6989  phplem3g  7037  nneneq  7038  ssfiexmid  7058  ssfiexmidt  7060  domfiexmid  7062  findcard  7072  findcard2  7073  findcard2s  7074  findcard2d  7075  findcard2sd  7076  diffifi  7078  ac6sfi  7082  fiintim  7118  fisseneq  7121  fidcenumlemrk  7147  fidcenumlemr  7148  isbth  7160  supeq3  7183  supeq123d  7184  supmoti  7186  suplubti  7193  supisolem  7201  cnvinfex  7211  eqinfti  7213  infvalti  7215  ordiso2  7228  nninfninc  7316  nnnninfeq2  7322  isomni  7329  finomni  7333  exmidomni  7335  ctssexmid  7343  ismkv  7346  ismkvnex  7348  mkvprop  7351  fodjumkvlemres  7352  enmkvlem  7354  iswomni  7358  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  tapeq1  7464  exmidapne  7472  ccfunen  7476  ltsonq  7611  ltexnqq  7621  prcdnql  7697  prcunqu  7698  prloc  7704  prdisj  7705  genprndl  7734  genprndu  7735  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemcl  7889  caucvgprprlemcbv  7900  caucvgprprlemval  7901  suplocexprlemloc  7934  lttrsr  7975  ltsosr  7977  recexgt0sr  7986  mulgt0sr  7991  aptisr  7992  mulextsr1  7994  srpospr  7996  caucvgsrlemgt1  8008  caucvgsrlemoffres  8013  caucvgsr  8015  map2psrprg  8018  suplocsrlemb  8019  axprecex  8093  axpre-ltwlin  8096  axpre-lttrn  8097  axpre-apti  8098  axpre-mulgt0  8100  axpre-mulext  8101  axcaucvglemcau  8111  axcaucvglemres  8112  axpre-suploclemres  8114  axpre-suploc  8115  axsuploc  8245  ltleletr  8254  ltordlem  8655  squeeze0  9077  sup3exmid  9130  nnsub  9175  fzind  9588  uzind4s  9817  uzind4s2  9818  indstr  9820  supinfneg  9822  infsupneg  9823  frec2uzuzd  10657  frec2uzltd  10658  uzsinds  10699  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  monoord  10740  seq3split  10743  seqsplitg  10744  seqf1oglem2  10775  seqf1og  10776  seq3id2  10781  seqhomog  10785  expcl2lemap  10806  nn0ltexp2  10964  facdiv  10993  facwordi  10995  zfz1isolem1  11097  zfz1iso  11098  seq3coll  11099  wrdind  11296  wrd2ind  11297  swrdccatin1  11299  swrdccat3blem  11313  reuccatpfxs1lem  11320  caucvgre  11535  fimaxre2  11781  climcn1  11862  climcn2  11863  subcn2  11865  summodclem2a  11935  fsumsplitf  11962  fsum2d  11989  modfsummod  12012  fsumabs  12019  telfsumo  12020  fsumiun  12031  prodfdivap  12101  fprod2d  12177  fproddivapf  12185  fprodsplitf  12186  fprodsplit1f  12188  ndvdssub  12484  bezoutlemmain  12562  bezoutlemex  12565  bezoutlemzz  12566  bezoutlemsup  12573  dfgcd2  12578  algcvg  12613  algcvga  12616  algfx  12617  lcmgcdlem  12642  lcmdvds  12644  coprmgcdb  12653  coprmdvds1  12656  coprmdvds2  12658  prmind2  12685  dvdsprime  12687  nprm  12688  dvdsprm  12702  exprmfct  12703  isprm5lem  12706  coprm  12709  isprm6  12712  prmfac1  12717  sqrt2irr  12727  pcqmul  12869  pcqcl  12872  pc2dvds  12896  pcz  12898  prmpwdvds  12921  ennnfonelemim  13038  exmidunben  13040  infpn2  13070  setscomd  13116  mhmlem  13694  isnsg2  13783  ghmf1  13853  islring  14199  lringuplu  14203  rrgval  14269  rrgeq0i  14271  isdomn  14276  domneq0  14279  opprdomnbg  14281  znidom  14664  znrrg  14667  mplvalcoe  14697  mplsubgfilemcl  14706  uniopn  14718  fiinopn  14721  epttop  14807  cnpval  14915  iscnp  14916  icnpimaex  14928  lmcvg  14934  cnptoprest  14956  cnptoprest2  14957  lmss  14963  lmff  14966  txcnp  14988  txlm  14996  cnmpt12  15004  cnmpt22  15011  blssps  15144  blss  15145  metss  15211  comet  15216  metcnp3  15228  metcnp2  15230  txmetcnp  15235  divcnap  15282  mpomulcn  15283  elcncf2  15291  cncfi  15295  mulc1cncf  15306  cncfmet  15309  mulcncflem  15324  mulcncf  15325  dedekindeulemloc  15336  dedekindeulemlu  15338  dedekindeulemeu  15339  suplociccreex  15341  dedekindicclemloc  15345  dedekindicclemlu  15347  dedekindicclemeu  15348  ivthinclemlopn  15353  ivthinclemlr  15354  ivthinclemuopn  15355  ivthinclemur  15356  ivthinclemloc  15358  ivthreinc  15362  limccl  15376  ellimc3apf  15377  limccnpcntop  15392  limccnp2lem  15393  limccoap  15395  dvcoapbr  15424  dvmptfsum  15442  mpodvdsmulf1o  15707  perfectlem2  15717  lgsdir2lem4  15753  gausslemma2dlem0i  15779  lgseisenlem2  15793  lgsquad2lem2  15804  2sqlem6  15842  2sqlem8  15845  2sqlem10  15847  gropd  15891  grstructd2dom  15892  upgredg2vtx  15992  upgredgpr  15993  cbvrald  16334  bj-bdfindes  16494  bj-omtrans  16501  bj-inf2vnlem1  16515  bj-inf2vnlem2  16516  bj-inf2vnlem3  16517  bj-inf2vnlem4  16518  bj-findes  16526  strcoll2  16528  sscoll2  16533  subctctexmid  16551  pw1nct  16554  exmidsbthrlem  16576  sbthom  16580  apdiff  16602  ismkvnnlem  16606  nconstwlpolem  16619  neapmkv  16622  neap0mkv  16623  ltlenmkv  16624