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  2849  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspc2gv  2919  ceqex  2930  ralab2  2967  mob2  2983  mob  2985  morex  2987  reu7  2998  reu8  2999  nelrdva  3010  cdeqim  3021  sbcimg  3070  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  sbcssg  3600  sneqrg  3839  elintab  3933  intss1  3937  intmin  3942  dfiin2g  3997  disji2  4074  disjiun  4077  trel  4188  trss  4190  bnd2  4256  zfpow  4258  exmidexmid  4279  exmidsssnc  4286  exmidundifim  4290  exmid1stab  4291  rext  4300  opth  4322  copsexg  4329  poeq1  4387  pocl  4391  swopolem  4393  swopo  4394  soeq1  4403  sowlin  4408  frforeq2  4433  frforeq3  4435  frirrg  4438  frind  4440  weeq1  4444  ordelord  4469  reusv3i  4547  ordtriexmid  4610  ontr2exmid  4614  onsucsssucexmid  4616  onsucelsucexmid  4619  ordsucunielexmid  4620  regexmidlem1  4622  regexmid  4624  reg2exmid  4625  elirr  4630  en2lp  4643  ordsoexmid  4651  onintexmid  4662  reg3exmid  4669  tfis  4672  tfisi  4676  peano2  4684  findes  4692  nnregexmid  4710  omsinds  4711  vtoclr  4764  poinxp  4785  soinxp  4786  posng  4788  ssrel  4804  ssrel2  4806  ssrelrel  4816  relop  4869  issref  5107  iotaexab  5293  iota5  5296  dffun4f  5330  sbcfung  5338  funopg  5348  brprcneu  5616  funfveu  5636  tz6.12f  5652  funbrfv  5664  ssimaexg  5689  fvmptss2  5702  fvmptssdm  5712  fvmptf  5720  fvelrn  5759  f1veqaeq  5886  dff13f  5887  isopolem  5939  isosolem  5941  riota5f  5974  imbrov2fvoveq  6019  oprabid  6026  ovmpos  6119  ov2gf  6120  ovi3  6133  caovcan  6161  caovordig  6162  caofrss  6240  caoftrn  6241  dfoprab4f  6329  f1o2ndf1  6364  poxp  6368  smoel  6436  tfrlem1  6444  tfr1onlemsucfn  6476  tfr1onlemsucaccv  6477  tfr1onlembxssdm  6479  tfr1onlembfn  6480  tfr1onlemaccex  6484  tfr1onlemres  6485  tfrcllemsucfn  6489  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllembfn  6493  tfrcllemaccex  6497  tfrcllemres  6498  tfrcl  6500  nnsucelsuc  6627  nnsucsssuc  6628  nnmordi  6652  nnaordex  6664  qsel  6749  eroveu  6763  ecopovtrn  6769  ecopovtrng  6772  th3qlem2  6775  ixpsnf1o  6873  fundmeng  6950  phplem3g  7005  nneneq  7006  ssfiexmid  7026  domfiexmid  7028  findcard  7038  findcard2  7039  findcard2s  7040  findcard2d  7041  findcard2sd  7042  diffifi  7044  ac6sfi  7048  fiintim  7081  fisseneq  7084  fidcenumlemrk  7109  fidcenumlemr  7110  isbth  7122  supeq3  7145  supeq123d  7146  supmoti  7148  suplubti  7155  supisolem  7163  cnvinfex  7173  eqinfti  7175  infvalti  7177  ordiso2  7190  nninfninc  7278  nnnninfeq2  7284  isomni  7291  finomni  7295  exmidomni  7297  ctssexmid  7305  ismkv  7308  ismkvnex  7310  mkvprop  7313  fodjumkvlemres  7314  enmkvlem  7316  iswomni  7320  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  tapeq1  7426  exmidapne  7434  ccfunen  7438  ltsonq  7573  ltexnqq  7583  prcdnql  7659  prcunqu  7660  prloc  7666  prdisj  7667  genprndl  7696  genprndu  7697  caucvgprlemnkj  7841  caucvgprlemnbj  7842  caucvgprlemcl  7851  caucvgprprlemcbv  7862  caucvgprprlemval  7863  suplocexprlemloc  7896  lttrsr  7937  ltsosr  7939  recexgt0sr  7948  mulgt0sr  7953  aptisr  7954  mulextsr1  7956  srpospr  7958  caucvgsrlemgt1  7970  caucvgsrlemoffres  7975  caucvgsr  7977  map2psrprg  7980  suplocsrlemb  7981  axprecex  8055  axpre-ltwlin  8058  axpre-lttrn  8059  axpre-apti  8060  axpre-mulgt0  8062  axpre-mulext  8063  axcaucvglemcau  8073  axcaucvglemres  8074  axpre-suploclemres  8076  axpre-suploc  8077  axsuploc  8207  ltleletr  8216  ltordlem  8617  squeeze0  9039  sup3exmid  9092  nnsub  9137  fzind  9550  uzind4s  9773  uzind4s2  9774  indstr  9776  supinfneg  9778  infsupneg  9779  frec2uzuzd  10611  frec2uzltd  10612  uzsinds  10653  seq3fveq2  10684  seqfveq2g  10686  seq3shft2  10690  seqshft2g  10691  monoord  10694  seq3split  10697  seqsplitg  10698  seqf1oglem2  10729  seqf1og  10730  seq3id2  10735  seqhomog  10739  expcl2lemap  10760  nn0ltexp2  10918  facdiv  10947  facwordi  10949  zfz1isolem1  11049  zfz1iso  11050  seq3coll  11051  wrdind  11240  wrd2ind  11241  swrdccatin1  11243  swrdccat3blem  11257  reuccatpfxs1lem  11264  caucvgre  11478  fimaxre2  11724  climcn1  11805  climcn2  11806  subcn2  11808  summodclem2a  11878  fsumsplitf  11905  fsum2d  11932  modfsummod  11955  fsumabs  11962  telfsumo  11963  fsumiun  11974  prodfdivap  12044  fprod2d  12120  fproddivapf  12128  fprodsplitf  12129  fprodsplit1f  12131  ndvdssub  12427  bezoutlemmain  12505  bezoutlemex  12508  bezoutlemzz  12509  bezoutlemsup  12516  dfgcd2  12521  algcvg  12556  algcvga  12559  algfx  12560  lcmgcdlem  12585  lcmdvds  12587  coprmgcdb  12596  coprmdvds1  12599  coprmdvds2  12601  prmind2  12628  dvdsprime  12630  nprm  12631  dvdsprm  12645  exprmfct  12646  isprm5lem  12649  coprm  12652  isprm6  12655  prmfac1  12660  sqrt2irr  12670  pcqmul  12812  pcqcl  12815  pc2dvds  12839  pcz  12841  prmpwdvds  12864  ennnfonelemim  12981  exmidunben  12983  infpn2  13013  setscomd  13059  mhmlem  13637  isnsg2  13726  ghmf1  13796  islring  14141  lringuplu  14145  rrgval  14211  rrgeq0i  14213  isdomn  14218  domneq0  14221  opprdomnbg  14223  znidom  14606  znrrg  14609  mplvalcoe  14639  mplsubgfilemcl  14648  uniopn  14660  fiinopn  14663  epttop  14749  cnpval  14857  iscnp  14858  icnpimaex  14870  lmcvg  14876  cnptoprest  14898  cnptoprest2  14899  lmss  14905  lmff  14908  txcnp  14930  txlm  14938  cnmpt12  14946  cnmpt22  14953  blssps  15086  blss  15087  metss  15153  comet  15158  metcnp3  15170  metcnp2  15172  txmetcnp  15177  divcnap  15224  mpomulcn  15225  elcncf2  15233  cncfi  15237  mulc1cncf  15248  cncfmet  15251  mulcncflem  15266  mulcncf  15267  dedekindeulemloc  15278  dedekindeulemlu  15280  dedekindeulemeu  15281  suplociccreex  15283  dedekindicclemloc  15287  dedekindicclemlu  15289  dedekindicclemeu  15290  ivthinclemlopn  15295  ivthinclemlr  15296  ivthinclemuopn  15297  ivthinclemur  15298  ivthinclemloc  15300  ivthreinc  15304  limccl  15318  ellimc3apf  15319  limccnpcntop  15334  limccnp2lem  15335  limccoap  15337  dvcoapbr  15366  dvmptfsum  15384  mpodvdsmulf1o  15649  perfectlem2  15659  lgsdir2lem4  15695  gausslemma2dlem0i  15721  lgseisenlem2  15735  lgsquad2lem2  15746  2sqlem6  15784  2sqlem8  15787  2sqlem10  15789  gropd  15833  grstructd2dom  15834  upgredg2vtx  15931  upgredgpr  15932  cbvrald  16082  bj-bdfindes  16242  bj-omtrans  16249  bj-inf2vnlem1  16263  bj-inf2vnlem2  16264  bj-inf2vnlem3  16265  bj-inf2vnlem4  16266  bj-findes  16274  strcoll2  16276  sscoll2  16281  subctctexmid  16297  pw1nct  16300  exmidsbthrlem  16321  sbthom  16325  apdiff  16347  ismkvnnlem  16351  nconstwlpolem  16364  neapmkv  16367  neap0mkv  16368  ltlenmkv  16369