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  844  nfbidf  1592  drnf1  1786  drnf2  1787  equveli  1812  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  mobidh  2120  mobid  2121  axext3  2221  cbvralfw  2775  cbvralf  2777  cbvralvw  2790  cbvraldva2  2793  gencbval  2871  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  rspc2gv  2942  ceqex  2953  ralab2  2990  mob2  3006  mob  3008  morex  3010  reu7  3021  reu8  3022  nelrdva  3033  cdeqim  3044  sbcimg  3093  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  sbcssg  3636  ifeqeqxdc  3687  sneqrg  3885  elintab  3979  intss1  3983  intmin  3988  dfiin2g  4043  disji2  4120  disjiun  4123  trel  4234  trss  4236  bnd2  4308  zfpow  4310  exmidexmid  4331  exmidsssnc  4338  exmidundifim  4342  exmid1stab  4343  rext  4353  opth  4375  copsexg  4382  poeq1  4442  pocl  4446  swopolem  4448  swopo  4449  soeq1  4458  sowlin  4463  frforeq2  4488  frforeq3  4490  frirrg  4493  frind  4495  weeq1  4499  ordelord  4524  reusv3i  4603  ordtriexmid  4666  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmid  4675  ordsucunielexmid  4676  regexmidlem1  4678  regexmid  4680  reg2exmid  4681  elirr  4686  en2lp  4699  ordsoexmid  4707  onintexmid  4718  reg3exmid  4725  tfis  4728  tfisi  4732  peano2  4740  findes  4748  nnregexmid  4766  omsinds  4767  vtoclr  4821  poinxp  4842  soinxp  4843  posng  4845  ssrel  4861  ssrel2  4863  ssrelrel  4873  relop  4928  issref  5168  iotaexab  5354  iota5  5357  dffun4f  5391  sbcfung  5399  funopg  5409  brprcneu  5686  funfveu  5706  tz6.12f  5722  funbrfv  5736  ssimaexg  5762  fvmptss2  5777  fvmptssdm  5787  fvmptf  5795  fvelrn  5833  f1veqaeq  5969  dff13f  5970  isopolem  6022  isosolem  6024  riota5f  6059  imbrov2fvoveq  6104  oprabid  6111  ovmpos  6206  ov2gf  6207  ovi3  6220  caovcan  6248  caovordig  6249  caofrss  6328  caoftrn  6329  dfoprab4f  6421  f1o2ndf1  6458  poxp  6462  suppfnss  6491  smoel  6565  tfrlem1  6573  tfr1onlemsucfn  6605  tfr1onlemsucaccv  6606  tfr1onlembxssdm  6608  tfr1onlembfn  6609  tfr1onlemaccex  6613  tfr1onlemres  6614  tfrcllemsucfn  6618  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllembfn  6622  tfrcllemaccex  6626  tfrcllemres  6627  tfrcl  6629  nnsucelsuc  6758  nnsucsssuc  6759  nnmordi  6783  nnaordex  6795  qsel  6880  eroveu  6894  ecopovtrn  6900  ecopovtrng  6903  th3qlem2  6906  ixpsnf1o  7012  fundmeng  7089  modom  7102  phplem3g  7151  nneneq  7152  ssfiexmid  7172  ssfiexmidt  7174  domfiexmid  7176  findcard  7186  findcard2  7187  findcard2s  7188  findcard2d  7189  findcard2sd  7190  diffifi  7192  ac6sfi  7196  fiintim  7232  fisseneq  7236  fidcenumlemrk  7265  fidcenumlemr  7266  isbth  7278  supeq3  7324  supeq123d  7325  supmoti  7327  suplubti  7334  supisolem  7342  cnvinfex  7352  eqinfti  7354  infvalti  7356  ordiso2  7369  nninfninc  7457  nnnninfeq2  7463  isomni  7470  finomni  7474  exmidomni  7476  ctssexmid  7484  ismkv  7487  ismkvnex  7489  mkvprop  7492  fodjumkvlemres  7493  enmkvlem  7495  iswomni  7499  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  papeq1  7603  papsym  7606  papcotr  7607  tapeq1  7612  exmidapne  7620  ccfunen  7624  ltsonq  7759  ltexnqq  7769  prcdnql  7845  prcunqu  7846  prloc  7852  prdisj  7853  genprndl  7882  genprndu  7883  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemcl  8037  caucvgprprlemcbv  8048  caucvgprprlemval  8049  suplocexprlemloc  8082  lttrsr  8123  ltsosr  8125  recexgt0sr  8134  mulgt0sr  8139  aptisr  8140  mulextsr1  8142  srpospr  8144  caucvgsrlemgt1  8156  caucvgsrlemoffres  8161  caucvgsr  8163  map2psrprg  8166  suplocsrlemb  8167  axprecex  8241  axpre-ltwlin  8244  axpre-lttrn  8245  axpre-apti  8246  axpre-mulgt0  8248  axpre-mulext  8249  axcaucvglemcau  8259  axcaucvglemres  8260  axpre-suploclemres  8262  axpre-suploc  8263  axsuploc  8392  ltleletr  8401  ltordlem  8804  squeeze0  9228  sup3exmid  9281  nnsub  9326  fzind  9744  uzind4s  9973  uzind4s2  9974  indstr  9976  supinfneg  9978  infsupneg  9979  frec2uzuzd  10822  frec2uzltd  10823  uzsinds  10864  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  monoord  10905  seq3split  10908  seqsplitg  10909  seqf1oglem2  10940  seqf1og  10941  seq3id2  10946  seqhomog  10950  expcl2lemap  10971  nn0ltexp2  11130  facdiv  11159  facwordi  11161  zfz1isolem1  11275  zfz1iso  11276  seq3coll  11277  wrdind  11477  wrd2ind  11478  swrdccatin1  11480  swrdccat3blem  11494  reuccatpfxs1lem  11501  caucvgre  11730  fimaxre2  11976  climcn1  12057  climcn2  12058  subcn2  12060  summodclem2a  12131  fsumsplitf  12158  fsum2d  12185  modfsummod  12208  fsumabs  12215  telfsumo  12216  fsumiun  12227  prodfdivap  12297  fprod2d  12373  fproddivapf  12381  fprodsplitf  12382  fprodsplit1f  12384  ndvdssub  12680  bezoutlemmain  12758  bezoutlemex  12761  bezoutlemzz  12762  bezoutlemsup  12769  dfgcd2  12774  algcvg  12809  algcvga  12812  algfx  12813  lcmgcdlem  12838  lcmdvds  12840  coprmgcdb  12849  coprmdvds1  12852  coprmdvds2  12854  prmind2  12881  dvdsprime  12883  nprm  12884  dvdsprm  12898  exprmfct  12899  isprm5lem  12902  coprm  12905  isprm6  12908  prmfac1  12913  sqrt2irr  12923  pcqmul  13065  pcqcl  13068  pc2dvds  13092  pcz  13094  prmpwdvds  13117  ballotfilem2  13211  ennnfonelemim  13298  exmidunben  13300  infpn2  13330  setscomd  13376  mhmlem  13900  isnsg2  13989  ghmf1  14059  islring  14482  lringuplu  14486  opprlring  14487  rrgval  14553  rrgeq0i  14555  isdomn  14561  domneq0  14564  opprdomnbg  14566  znidom  14975  znrrg  14978  mplvalcoe  15064  mplsubgfilemcl  15073  uniopn  15085  fiinopn  15088  epttop  15174  cnpval  15282  iscnp  15283  icnpimaex  15295  lmcvg  15301  cnptoprest  15323  cnptoprest2  15324  lmss  15330  lmff  15333  txcnp  15355  txlm  15363  cnmpt12  15371  cnmpt22  15378  blssps  15511  blss  15512  metss  15578  comet  15583  metcnp3  15595  metcnp2  15597  txmetcnp  15602  divcnap  15649  mpomulcn  15650  elcncf2  15658  cncfi  15662  mulc1cncf  15673  cncfmet  15676  mulcncflem  15691  mulcncf  15692  dedekindeulemloc  15703  dedekindeulemlu  15705  dedekindeulemeu  15706  suplociccreex  15708  dedekindicclemloc  15712  dedekindicclemlu  15714  dedekindicclemeu  15715  ivthinclemlopn  15720  ivthinclemlr  15721  ivthinclemuopn  15722  ivthinclemur  15723  ivthinclemloc  15725  ivthreinc  15729  limccl  15743  ellimc3apf  15744  limccnpcntop  15759  limccnp2lem  15760  limccoap  15762  dvcoapbr  15791  dvmptfsum  15809  mpodvdsmulf1o  16087  perfectlem2  16097  lgsdir2lem4  16133  gausslemma2dlem0i  16159  lgseisenlem2  16173  lgsquad2lem2  16184  2sqlem6  16222  2sqlem8  16225  2sqlem10  16227  gropd  16271  grstructd2dom  16272  upgredg2vtx  16372  upgredgpr  16373  eupth2fi  16703  lealltlt1  16734  lealltlt2  16735  dichmul0orlem7  16742  cbvrald  16799  bj-bdfindes  16958  bj-omtrans  16965  bj-inf2vnlem1  16979  bj-inf2vnlem2  16980  bj-inf2vnlem3  16981  bj-inf2vnlem4  16982  bj-findes  16990  strcoll2  16992  sscoll2  16997  subctctexmid  17013  pw1nct  17016  exmidnotnotr  17018  exmidcon  17019  exmidsbthrlem  17041  sbthom  17045  apdiff  17071  ismkvnnlem  17076  nconstwlpolem  17089  neapmkv  17092  neap0mkv  17093  ltlenmkv  17094  alsbid  17117  cbvals  17120