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  8774  squeeze0  9198  sup3exmid  9251  nnsub  9296  fzind  9714  uzind4s  9943  uzind4s2  9944  indstr  9946  supinfneg  9948  infsupneg  9949  frec2uzuzd  10791  frec2uzltd  10792  uzsinds  10833  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seqf1oglem2  10909  seqf1og  10910  seq3id2  10915  seqhomog  10919  expcl2lemap  10940  nn0ltexp2  11099  facdiv  11128  facwordi  11130  zfz1isolem1  11240  zfz1iso  11241  seq3coll  11242  wrdind  11442  wrd2ind  11443  swrdccatin1  11445  swrdccat3blem  11459  reuccatpfxs1lem  11466  caucvgre  11695  fimaxre2  11941  climcn1  12022  climcn2  12023  subcn2  12025  summodclem2a  12096  fsumsplitf  12123  fsum2d  12150  modfsummod  12173  fsumabs  12180  telfsumo  12181  fsumiun  12192  prodfdivap  12262  fprod2d  12338  fproddivapf  12346  fprodsplitf  12347  fprodsplit1f  12349  ndvdssub  12645  bezoutlemmain  12723  bezoutlemex  12726  bezoutlemzz  12727  bezoutlemsup  12734  dfgcd2  12739  algcvg  12774  algcvga  12777  algfx  12778  lcmgcdlem  12803  lcmdvds  12805  coprmgcdb  12814  coprmdvds1  12817  coprmdvds2  12819  prmind2  12846  dvdsprime  12848  nprm  12849  dvdsprm  12863  exprmfct  12864  isprm5lem  12867  coprm  12870  isprm6  12873  prmfac1  12878  sqrt2irr  12888  pcqmul  13030  pcqcl  13033  pc2dvds  13057  pcz  13059  prmpwdvds  13082  ballotfilem2  13176  ennnfonelemim  13263  exmidunben  13265  infpn2  13295  setscomd  13341  mhmlem  13871  isnsg2  13960  ghmf1  14030  islring  14441  lringuplu  14445  opprlring  14446  rrgval  14512  rrgeq0i  14514  isdomn  14520  domneq0  14523  opprdomnbg  14525  znidom  14935  znrrg  14938  mplvalcoe  14975  mplsubgfilemcl  14984  uniopn  14996  fiinopn  14999  epttop  15085  cnpval  15193  iscnp  15194  icnpimaex  15206  lmcvg  15212  cnptoprest  15234  cnptoprest2  15235  lmss  15241  lmff  15244  txcnp  15266  txlm  15274  cnmpt12  15282  cnmpt22  15289  blssps  15422  blss  15423  metss  15489  comet  15494  metcnp3  15506  metcnp2  15508  txmetcnp  15513  divcnap  15560  mpomulcn  15561  elcncf2  15569  cncfi  15573  mulc1cncf  15584  cncfmet  15587  mulcncflem  15602  mulcncf  15603  dedekindeulemloc  15614  dedekindeulemlu  15616  dedekindeulemeu  15617  suplociccreex  15619  dedekindicclemloc  15623  dedekindicclemlu  15625  dedekindicclemeu  15626  ivthinclemlopn  15631  ivthinclemlr  15632  ivthinclemuopn  15633  ivthinclemur  15634  ivthinclemloc  15636  ivthreinc  15640  limccl  15654  ellimc3apf  15655  limccnpcntop  15670  limccnp2lem  15671  limccoap  15673  dvcoapbr  15702  dvmptfsum  15720  mpodvdsmulf1o  15988  perfectlem2  15998  lgsdir2lem4  16034  gausslemma2dlem0i  16060  lgseisenlem2  16074  lgsquad2lem2  16085  2sqlem6  16123  2sqlem8  16126  2sqlem10  16128  gropd  16172  grstructd2dom  16173  upgredg2vtx  16273  upgredgpr  16274  eupth2fi  16604  lealltlt1  16635  lealltlt2  16636  dichmul0orlem7  16643  cbvrald  16700  bj-bdfindes  16859  bj-omtrans  16866  bj-inf2vnlem1  16880  bj-inf2vnlem2  16881  bj-inf2vnlem3  16882  bj-inf2vnlem4  16883  bj-findes  16891  strcoll2  16893  sscoll2  16898  subctctexmid  16914  pw1nct  16917  exmidnotnotr  16919  exmidcon  16920  exmidsbthrlem  16942  sbthom  16946  apdiff  16972  ismkvnnlem  16977  nconstwlpolem  16990  neapmkv  16993  neap0mkv  16994  ltlenmkv  16995