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  832  nfbidf  1539  drnf1  1733  drnf2  1734  equveli  1759  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  mobidh  2060  mobid  2061  axext3  2160  cbvralfw  2694  cbvralf  2696  cbvralvw  2707  cbvraldva2  2710  gencbval  2785  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  rspct  2834  rspc  2835  rspc2gv  2853  ceqex  2864  ralab2  2901  mob2  2917  mob  2919  morex  2921  reu7  2932  reu8  2933  nelrdva  2944  cdeqim  2955  sbcimg  3004  csbhypf  3095  cbvralcsf  3119  dfss2f  3146  sbcssg  3532  sneqrg  3762  elintab  3855  intss1  3859  intmin  3864  dfiin2g  3919  disji2  3996  disjiun  3998  trel  4108  trss  4110  bnd2  4173  zfpow  4175  exmidexmid  4196  exmidsssnc  4203  exmidundifim  4207  exmid1stab  4208  rext  4215  opth  4237  copsexg  4244  poeq1  4299  pocl  4303  swopolem  4305  swopo  4306  soeq1  4315  sowlin  4320  frforeq2  4345  frforeq3  4347  frirrg  4350  frind  4352  weeq1  4356  ordelord  4381  reusv3i  4459  ordtriexmid  4520  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmid  4529  ordsucunielexmid  4530  regexmidlem1  4532  regexmid  4534  reg2exmid  4535  elirr  4540  en2lp  4553  ordsoexmid  4561  onintexmid  4572  reg3exmid  4579  tfis  4582  tfisi  4586  peano2  4594  findes  4602  nnregexmid  4620  omsinds  4621  vtoclr  4674  poinxp  4695  soinxp  4696  posng  4698  ssrel  4714  ssrel2  4716  ssrelrel  4726  relop  4777  issref  5011  iota5  5198  dffun4f  5232  sbcfung  5240  funopg  5250  brprcneu  5508  funfveu  5528  tz6.12f  5544  funbrfv  5554  ssimaexg  5578  fvmptss2  5591  fvmptssdm  5600  fvmptf  5608  fvelrn  5647  f1veqaeq  5769  dff13f  5770  isopolem  5822  isosolem  5824  riota5f  5854  imbrov2fvoveq  5899  oprabid  5906  ovmpos  5997  ov2gf  5998  ovi3  6010  caovcan  6038  caovordig  6039  caofrss  6106  caoftrn  6107  dfoprab4f  6193  f1o2ndf1  6228  poxp  6232  smoel  6300  tfrlem1  6308  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemaccex  6348  tfr1onlemres  6349  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemaccex  6361  tfrcllemres  6362  tfrcl  6364  nnsucelsuc  6491  nnsucsssuc  6492  nnmordi  6516  nnaordex  6528  qsel  6611  eroveu  6625  ecopovtrn  6631  ecopovtrng  6634  th3qlem2  6637  ixpsnf1o  6735  fundmeng  6806  phplem3g  6855  nneneq  6856  ssfiexmid  6875  domfiexmid  6877  findcard  6887  findcard2  6888  findcard2s  6889  findcard2d  6890  findcard2sd  6891  diffifi  6893  ac6sfi  6897  fiintim  6927  fisseneq  6930  fidcenumlemrk  6952  fidcenumlemr  6953  isbth  6965  supeq3  6988  supeq123d  6989  supmoti  6991  suplubti  6998  supisolem  7006  cnvinfex  7016  eqinfti  7018  infvalti  7020  ordiso2  7033  nnnninfeq2  7126  isomni  7133  finomni  7137  exmidomni  7139  ctssexmid  7147  ismkv  7150  ismkvnex  7152  mkvprop  7155  fodjumkvlemres  7156  enmkvlem  7158  iswomni  7162  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  tapeq1  7250  exmidapne  7258  ccfunen  7262  ltsonq  7396  ltexnqq  7406  prcdnql  7482  prcunqu  7483  prloc  7489  prdisj  7490  genprndl  7519  genprndu  7520  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemcl  7674  caucvgprprlemcbv  7685  caucvgprprlemval  7686  suplocexprlemloc  7719  lttrsr  7760  ltsosr  7762  recexgt0sr  7771  mulgt0sr  7776  aptisr  7777  mulextsr1  7779  srpospr  7781  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  map2psrprg  7803  suplocsrlemb  7804  axprecex  7878  axpre-ltwlin  7881  axpre-lttrn  7882  axpre-apti  7883  axpre-mulgt0  7885  axpre-mulext  7886  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  axpre-suploc  7900  axsuploc  8029  ltleletr  8038  ltordlem  8438  squeeze0  8860  sup3exmid  8913  nnsub  8957  fzind  9367  uzind4s  9589  uzind4s2  9590  indstr  9592  supinfneg  9594  infsupneg  9595  frec2uzuzd  10401  frec2uzltd  10402  uzsinds  10441  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  seq3id2  10508  expcl2lemap  10531  nn0ltexp2  10688  facdiv  10717  facwordi  10719  zfz1isolem1  10819  zfz1iso  10820  seq3coll  10821  caucvgre  10989  fimaxre2  11234  climcn1  11315  climcn2  11316  subcn2  11318  summodclem2a  11388  fsumsplitf  11415  fsum2d  11442  modfsummod  11465  fsumabs  11472  telfsumo  11473  fsumiun  11484  prodfdivap  11554  fprod2d  11630  fproddivapf  11638  fprodsplitf  11639  fprodsplit1f  11641  ndvdssub  11934  bezoutlemmain  11998  bezoutlemex  12001  bezoutlemzz  12002  bezoutlemsup  12009  dfgcd2  12014  algcvg  12047  algcvga  12050  algfx  12051  lcmgcdlem  12076  lcmdvds  12078  coprmgcdb  12087  coprmdvds1  12090  coprmdvds2  12092  prmind2  12119  dvdsprime  12121  nprm  12122  dvdsprm  12136  exprmfct  12137  isprm5lem  12140  coprm  12143  isprm6  12146  prmfac1  12151  sqrt2irr  12161  pcqmul  12302  pcqcl  12305  pc2dvds  12328  pcz  12330  prmpwdvds  12352  ennnfonelemim  12424  exmidunben  12426  infpn2  12456  setscomd  12502  mhmlem  12977  isnsg2  13061  islring  13331  lringuplu  13335  uniopn  13471  fiinopn  13474  epttop  13560  cnpval  13668  iscnp  13669  icnpimaex  13681  lmcvg  13687  cnptoprest  13709  cnptoprest2  13710  lmss  13716  lmff  13719  txcnp  13741  txlm  13749  cnmpt12  13757  cnmpt22  13764  blssps  13897  blss  13898  metss  13964  comet  13969  metcnp3  13981  metcnp2  13983  txmetcnp  13988  divcnap  14025  elcncf2  14031  cncfi  14035  mulc1cncf  14046  cncfmet  14049  mulcncflem  14060  mulcncf  14061  dedekindeulemloc  14067  dedekindeulemlu  14069  dedekindeulemeu  14070  suplociccreex  14072  dedekindicclemloc  14076  dedekindicclemlu  14078  dedekindicclemeu  14079  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  limccl  14098  ellimc3apf  14099  limccnpcntop  14114  limccnp2lem  14115  limccoap  14117  dvcoapbr  14141  lgsdir2lem4  14402  lgseisenlem2  14421  2sqlem6  14437  2sqlem8  14440  2sqlem10  14442  cbvrald  14510  bj-bdfindes  14671  bj-omtrans  14678  bj-inf2vnlem1  14692  bj-inf2vnlem2  14693  bj-inf2vnlem3  14694  bj-inf2vnlem4  14695  bj-findes  14703  strcoll2  14705  sscoll2  14710  subctctexmid  14720  pw1nct  14722  exmidsbthrlem  14740  sbthom  14744  apdiff  14766  ismkvnnlem  14770  nconstwlpolem  14782  neapmkv  14785  neap0mkv  14786  ltlenmkv  14787