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  840  nfbidf  1588  drnf1  1782  drnf2  1783  equveli  1808  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  mobidh  2116  mobid  2117  axext3  2217  cbvralfw  2769  cbvralf  2771  cbvralvw  2784  cbvraldva2  2787  gencbval  2865  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  rspct  2916  rspc  2917  rspc2gv  2936  ceqex  2947  ralab2  2984  mob2  3000  mob  3002  morex  3004  reu7  3015  reu8  3016  nelrdva  3027  cdeqim  3038  sbcimg  3087  csbhypf  3180  cbvralcsf  3204  dfssf  3232  dfss2f  3233  sbcssg  3622  ifeqeqxdc  3673  sneqrg  3871  elintab  3965  intss1  3969  intmin  3974  dfiin2g  4029  disji2  4106  disjiun  4109  trel  4220  trss  4222  bnd2  4291  zfpow  4293  exmidexmid  4314  exmidsssnc  4321  exmidundifim  4325  exmid1stab  4326  rext  4336  opth  4358  copsexg  4365  poeq1  4425  pocl  4429  swopolem  4431  swopo  4432  soeq1  4441  sowlin  4446  frforeq2  4471  frforeq3  4473  frirrg  4476  frind  4478  weeq1  4482  ordelord  4507  reusv3i  4585  ordtriexmid  4648  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  ordsucunielexmid  4658  regexmidlem1  4660  regexmid  4662  reg2exmid  4663  elirr  4668  en2lp  4681  ordsoexmid  4689  onintexmid  4700  reg3exmid  4707  tfis  4710  tfisi  4714  peano2  4722  findes  4730  nnregexmid  4748  omsinds  4749  vtoclr  4803  poinxp  4824  soinxp  4825  posng  4827  ssrel  4843  ssrel2  4845  ssrelrel  4855  relop  4910  issref  5150  iotaexab  5336  iota5  5339  dffun4f  5373  sbcfung  5381  funopg  5391  brprcneu  5668  funfveu  5688  tz6.12f  5704  funbrfv  5718  ssimaexg  5744  fvmptss2  5757  fvmptssdm  5767  fvmptf  5775  fvelrn  5813  f1veqaeq  5948  dff13f  5949  isopolem  6001  isosolem  6003  riota5f  6038  imbrov2fvoveq  6083  oprabid  6090  ovmpos  6185  ov2gf  6186  ovi3  6199  caovcan  6227  caovordig  6228  caofrss  6307  caoftrn  6308  dfoprab4f  6400  f1o2ndf1  6437  poxp  6441  suppfnss  6470  smoel  6544  tfrlem1  6552  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  nnsucelsuc  6737  nnsucsssuc  6738  nnmordi  6762  nnaordex  6774  qsel  6859  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem2  6885  ixpsnf1o  6984  fundmeng  7061  modom  7074  phplem3g  7123  nneneq  7124  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  findcard  7158  findcard2  7159  findcard2s  7160  findcard2d  7161  findcard2sd  7162  diffifi  7164  ac6sfi  7168  fiintim  7204  fisseneq  7208  fidcenumlemrk  7237  fidcenumlemr  7238  isbth  7250  supeq3  7294  supeq123d  7295  supmoti  7297  suplubti  7304  supisolem  7312  cnvinfex  7322  eqinfti  7324  infvalti  7326  ordiso2  7339  nninfninc  7427  nnnninfeq2  7433  isomni  7440  finomni  7444  exmidomni  7446  ctssexmid  7454  ismkv  7457  ismkvnex  7459  mkvprop  7462  fodjumkvlemres  7463  enmkvlem  7465  iswomni  7469  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  papeq1  7573  papsym  7576  papcotr  7577  tapeq1  7582  exmidapne  7590  ccfunen  7594  ltsonq  7729  ltexnqq  7739  prcdnql  7815  prcunqu  7816  prloc  7822  prdisj  7823  genprndl  7852  genprndu  7853  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemcl  8007  caucvgprprlemcbv  8018  caucvgprprlemval  8019  suplocexprlemloc  8052  lttrsr  8093  ltsosr  8095  recexgt0sr  8104  mulgt0sr  8109  aptisr  8110  mulextsr1  8112  srpospr  8114  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  map2psrprg  8136  suplocsrlemb  8137  axprecex  8211  axpre-ltwlin  8214  axpre-lttrn  8215  axpre-apti  8216  axpre-mulgt0  8218  axpre-mulext  8219  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  axsuploc  8362  ltleletr  8371  ltordlem  8773  squeeze0  9195  sup3exmid  9248  nnsub  9293  fzind  9711  uzind4s  9940  uzind4s2  9941  indstr  9943  supinfneg  9945  infsupneg  9946  frec2uzuzd  10788  frec2uzltd  10789  uzsinds  10830  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seqf1oglem2  10906  seqf1og  10907  seq3id2  10912  seqhomog  10916  expcl2lemap  10937  nn0ltexp2  11096  facdiv  11125  facwordi  11127  zfz1isolem1  11237  zfz1iso  11238  seq3coll  11239  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  swrdccat3blem  11456  reuccatpfxs1lem  11463  caucvgre  11691  fimaxre2  11937  climcn1  12018  climcn2  12019  subcn2  12021  summodclem2a  12092  fsumsplitf  12119  fsum2d  12146  modfsummod  12169  fsumabs  12176  telfsumo  12177  fsumiun  12188  prodfdivap  12258  fprod2d  12334  fproddivapf  12342  fprodsplitf  12343  fprodsplit1f  12345  ndvdssub  12641  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemsup  12730  dfgcd2  12735  algcvg  12770  algcvga  12773  algfx  12774  lcmgcdlem  12799  lcmdvds  12801  coprmgcdb  12810  coprmdvds1  12813  coprmdvds2  12815  prmind2  12842  dvdsprime  12844  nprm  12845  dvdsprm  12859  exprmfct  12860  isprm5lem  12863  coprm  12866  isprm6  12869  prmfac1  12874  sqrt2irr  12884  pcqmul  13026  pcqcl  13029  pc2dvds  13053  pcz  13055  prmpwdvds  13078  ballotfilem2  13172  ennnfonelemim  13259  exmidunben  13261  infpn2  13291  setscomd  13337  mhmlem  13915  isnsg2  14004  ghmf1  14074  islring  14422  lringuplu  14426  opprlring  14427  rrgval  14493  rrgeq0i  14495  isdomn  14501  domneq0  14504  opprdomnbg  14506  znidom  14917  znrrg  14920  mplvalcoe  14957  mplsubgfilemcl  14966  uniopn  14978  fiinopn  14981  epttop  15067  cnpval  15175  iscnp  15176  icnpimaex  15188  lmcvg  15194  cnptoprest  15216  cnptoprest2  15217  lmss  15223  lmff  15226  txcnp  15248  txlm  15256  cnmpt12  15264  cnmpt22  15271  blssps  15404  blss  15405  metss  15471  comet  15476  metcnp3  15488  metcnp2  15490  txmetcnp  15495  divcnap  15542  mpomulcn  15543  elcncf2  15551  cncfi  15555  mulc1cncf  15566  cncfmet  15569  mulcncflem  15584  mulcncf  15585  dedekindeulemloc  15596  dedekindeulemlu  15598  dedekindeulemeu  15599  suplociccreex  15601  dedekindicclemloc  15605  dedekindicclemlu  15607  dedekindicclemeu  15608  ivthinclemlopn  15613  ivthinclemlr  15614  ivthinclemuopn  15615  ivthinclemur  15616  ivthinclemloc  15618  ivthreinc  15622  limccl  15636  ellimc3apf  15637  limccnpcntop  15652  limccnp2lem  15653  limccoap  15655  dvcoapbr  15684  dvmptfsum  15702  mpodvdsmulf1o  15970  perfectlem2  15980  lgsdir2lem4  16016  gausslemma2dlem0i  16042  lgseisenlem2  16056  lgsquad2lem2  16067  2sqlem6  16105  2sqlem8  16108  2sqlem10  16110  gropd  16154  grstructd2dom  16155  upgredg2vtx  16255  upgredgpr  16256  eupth2fi  16586  cbvrald  16672  bj-bdfindes  16831  bj-omtrans  16838  bj-inf2vnlem1  16852  bj-inf2vnlem2  16853  bj-inf2vnlem3  16854  bj-inf2vnlem4  16855  bj-findes  16863  strcoll2  16865  sscoll2  16870  subctctexmid  16886  pw1nct  16889  exmidnotnotr  16891  exmidcon  16892  exmidsbthrlem  16914  sbthom  16918  apdiff  16944  ismkvnnlem  16949  nconstwlpolem  16963  neapmkv  16966  neap0mkv  16967  ltlenmkv  16968