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  839  nfbidf  1587  drnf1  1781  drnf2  1782  equveli  1807  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  mobidh  2113  mobid  2114  axext3  2214  cbvralfw  2756  cbvralf  2758  cbvralvw  2771  cbvraldva2  2774  gencbval  2852  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  rspc2gv  2922  ceqex  2933  ralab2  2970  mob2  2986  mob  2988  morex  2990  reu7  3001  reu8  3002  nelrdva  3013  cdeqim  3024  sbcimg  3073  csbhypf  3166  cbvralcsf  3190  dfss2f  3218  sbcssg  3603  sneqrg  3845  elintab  3939  intss1  3943  intmin  3948  dfiin2g  4003  disji2  4080  disjiun  4083  trel  4194  trss  4196  bnd2  4263  zfpow  4265  exmidexmid  4286  exmidsssnc  4293  exmidundifim  4297  exmid1stab  4298  rext  4307  opth  4329  copsexg  4336  poeq1  4396  pocl  4400  swopolem  4402  swopo  4403  soeq1  4412  sowlin  4417  frforeq2  4442  frforeq3  4444  frirrg  4447  frind  4449  weeq1  4453  ordelord  4478  reusv3i  4556  ordtriexmid  4619  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  regexmid  4633  reg2exmid  4634  elirr  4639  en2lp  4652  ordsoexmid  4660  onintexmid  4671  reg3exmid  4678  tfis  4681  tfisi  4685  peano2  4693  findes  4701  nnregexmid  4719  omsinds  4720  vtoclr  4774  poinxp  4795  soinxp  4796  posng  4798  ssrel  4814  ssrel2  4816  ssrelrel  4826  relop  4880  issref  5119  iotaexab  5305  iota5  5308  dffun4f  5342  sbcfung  5350  funopg  5360  brprcneu  5632  funfveu  5652  tz6.12f  5668  funbrfv  5682  ssimaexg  5708  fvmptss2  5721  fvmptssdm  5731  fvmptf  5739  fvelrn  5778  f1veqaeq  5910  dff13f  5911  isopolem  5963  isosolem  5965  riota5f  5998  imbrov2fvoveq  6043  oprabid  6050  ovmpos  6145  ov2gf  6146  ovi3  6159  caovcan  6187  caovordig  6188  caofrss  6267  caoftrn  6268  dfoprab4f  6356  f1o2ndf1  6393  poxp  6397  smoel  6466  tfrlem1  6474  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  nnsucelsuc  6659  nnsucsssuc  6660  nnmordi  6684  nnaordex  6696  qsel  6781  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem2  6807  ixpsnf1o  6905  fundmeng  6982  modom  6994  phplem3g  7042  nneneq  7043  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard  7077  findcard2  7078  findcard2s  7079  findcard2d  7080  findcard2sd  7081  diffifi  7083  ac6sfi  7087  fiintim  7123  fisseneq  7127  fidcenumlemrk  7153  fidcenumlemr  7154  isbth  7166  supeq3  7189  supeq123d  7190  supmoti  7192  suplubti  7199  supisolem  7207  cnvinfex  7217  eqinfti  7219  infvalti  7221  ordiso2  7234  nninfninc  7322  nnnninfeq2  7328  isomni  7335  finomni  7339  exmidomni  7341  ctssexmid  7349  ismkv  7352  ismkvnex  7354  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  iswomni  7364  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  tapeq1  7471  exmidapne  7479  ccfunen  7483  ltsonq  7618  ltexnqq  7628  prcdnql  7704  prcunqu  7705  prloc  7711  prdisj  7712  genprndl  7741  genprndu  7742  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgprprlemcbv  7907  caucvgprprlemval  7908  suplocexprlemloc  7941  lttrsr  7982  ltsosr  7984  recexgt0sr  7993  mulgt0sr  7998  aptisr  7999  mulextsr1  8001  srpospr  8003  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  map2psrprg  8025  suplocsrlemb  8026  axprecex  8100  axpre-ltwlin  8103  axpre-lttrn  8104  axpre-apti  8105  axpre-mulgt0  8107  axpre-mulext  8108  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  axsuploc  8252  ltleletr  8261  ltordlem  8662  squeeze0  9084  sup3exmid  9137  nnsub  9182  fzind  9595  uzind4s  9824  uzind4s2  9825  indstr  9827  supinfneg  9829  infsupneg  9830  frec2uzuzd  10665  frec2uzltd  10666  uzsinds  10707  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seqf1oglem2  10783  seqf1og  10784  seq3id2  10789  seqhomog  10793  expcl2lemap  10814  nn0ltexp2  10972  facdiv  11001  facwordi  11003  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccat3blem  11324  reuccatpfxs1lem  11331  caucvgre  11546  fimaxre2  11792  climcn1  11873  climcn2  11874  subcn2  11876  summodclem2a  11947  fsumsplitf  11974  fsum2d  12001  modfsummod  12024  fsumabs  12031  telfsumo  12032  fsumiun  12043  prodfdivap  12113  fprod2d  12189  fproddivapf  12197  fprodsplitf  12198  fprodsplit1f  12200  ndvdssub  12496  bezoutlemmain  12574  bezoutlemex  12577  bezoutlemzz  12578  bezoutlemsup  12585  dfgcd2  12590  algcvg  12625  algcvga  12628  algfx  12629  lcmgcdlem  12654  lcmdvds  12656  coprmgcdb  12665  coprmdvds1  12668  coprmdvds2  12670  prmind2  12697  dvdsprime  12699  nprm  12700  dvdsprm  12714  exprmfct  12715  isprm5lem  12718  coprm  12721  isprm6  12724  prmfac1  12729  sqrt2irr  12739  pcqmul  12881  pcqcl  12884  pc2dvds  12908  pcz  12910  prmpwdvds  12933  ennnfonelemim  13050  exmidunben  13052  infpn2  13082  setscomd  13128  mhmlem  13706  isnsg2  13795  ghmf1  13865  islring  14212  lringuplu  14216  rrgval  14282  rrgeq0i  14284  isdomn  14289  domneq0  14292  opprdomnbg  14294  znidom  14677  znrrg  14680  mplvalcoe  14710  mplsubgfilemcl  14719  uniopn  14731  fiinopn  14734  epttop  14820  cnpval  14928  iscnp  14929  icnpimaex  14941  lmcvg  14947  cnptoprest  14969  cnptoprest2  14970  lmss  14976  lmff  14979  txcnp  15001  txlm  15009  cnmpt12  15017  cnmpt22  15024  blssps  15157  blss  15158  metss  15224  comet  15229  metcnp3  15241  metcnp2  15243  txmetcnp  15248  divcnap  15295  mpomulcn  15296  elcncf2  15304  cncfi  15308  mulc1cncf  15319  cncfmet  15322  mulcncflem  15337  mulcncf  15338  dedekindeulemloc  15349  dedekindeulemlu  15351  dedekindeulemeu  15352  suplociccreex  15354  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicclemeu  15361  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemloc  15371  ivthreinc  15375  limccl  15389  ellimc3apf  15390  limccnpcntop  15405  limccnp2lem  15406  limccoap  15408  dvcoapbr  15437  dvmptfsum  15455  mpodvdsmulf1o  15720  perfectlem2  15730  lgsdir2lem4  15766  gausslemma2dlem0i  15792  lgseisenlem2  15806  lgsquad2lem2  15817  2sqlem6  15855  2sqlem8  15858  2sqlem10  15860  gropd  15904  grstructd2dom  15905  upgredg2vtx  16005  upgredgpr  16006  eupth2fi  16336  cbvrald  16410  bj-bdfindes  16570  bj-omtrans  16577  bj-inf2vnlem1  16591  bj-inf2vnlem2  16592  bj-inf2vnlem3  16593  bj-inf2vnlem4  16594  bj-findes  16602  strcoll2  16604  sscoll2  16609  subctctexmid  16627  pw1nct  16630  exmidsbthrlem  16652  sbthom  16656  apdiff  16678  ismkvnnlem  16682  nconstwlpolem  16695  neapmkv  16698  neap0mkv  16699  ltlenmkv  16700