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 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3887  elintab  3981  intss1  3985  intmin  3990  dfiin2g  4045  disji2  4122  disjiun  4125  trel  4236  trss  4238  bnd2  4310  zfpow  4312  exmidexmid  4333  exmidsssnc  4340  exmidundifim  4344  exmid1stab  4345  rext  4355  opth  4377  copsexg  4384  poeq1  4444  pocl  4448  swopolem  4450  swopo  4451  soeq1  4460  sowlin  4465  frforeq2  4490  frforeq3  4492  frirrg  4495  frind  4497  weeq1  4501  ordelord  4526  reusv3i  4605  ordtriexmid  4668  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  regexmid  4682  reg2exmid  4683  elirr  4688  en2lp  4701  ordsoexmid  4709  onintexmid  4720  reg3exmid  4727  tfis  4730  tfisi  4734  peano2  4742  findes  4750  nnregexmid  4768  omsinds  4769  vtoclr  4823  poinxp  4844  soinxp  4845  posng  4847  ssrel  4863  ssrel2  4865  ssrelrel  4875  relop  4930  issref  5170  iotaexab  5356  iota5  5359  dffun4f  5393  sbcfung  5401  funopg  5411  brprcneu  5688  funfveu  5708  tz6.12f  5724  funbrfv  5739  ssimaexg  5765  fvmptss2  5780  fvmptssdm  5790  fvmptf  5798  fvelrn  5839  f1veqaeq  5975  dff13f  5976  isopolem  6028  isosolem  6030  riota5f  6065  imbrov2fvoveq  6110  oprabid  6117  ovmpos  6212  ov2gf  6213  ovi3  6226  caovcan  6254  caovordig  6255  caofrss  6334  caoftrn  6335  dfoprab4f  6427  f1o2ndf1  6464  poxp  6468  suppfnss  6497  smoel  6571  tfrlem1  6579  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  nnsucelsuc  6764  nnsucsssuc  6765  nnmordi  6789  nnaordex  6801  qsel  6886  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  ixpsnf1o  7018  fundmeng  7095  modom  7108  phplem3g  7157  nneneq  7158  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  diffifi  7198  ac6sfi  7202  fiintim  7238  fisseneq  7242  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  supeq3  7330  supeq123d  7331  supmoti  7333  suplubti  7340  supisolem  7348  cnvinfex  7358  eqinfti  7360  infvalti  7362  ordiso2  7375  nninfninc  7463  nnnninfeq2  7469  isomni  7476  finomni  7480  exmidomni  7482  ctssexmid  7490  ismkv  7493  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  iswomni  7505  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papeq1  7609  papsym  7612  papcotr  7613  tapeq1  7618  exmidapne  7626  ccfunen  7630  ltsonq  7765  ltexnqq  7775  prcdnql  7851  prcunqu  7852  prloc  7858  prdisj  7859  genprndl  7888  genprndu  7889  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgprprlemcbv  8054  caucvgprprlemval  8055  suplocexprlemloc  8088  lttrsr  8129  ltsosr  8131  recexgt0sr  8140  mulgt0sr  8145  aptisr  8146  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  suplocsrlemb  8173  axprecex  8247  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  axsuploc  8398  ltleletr  8407  ltordlem  8810  squeeze0  9235  sup3exmid  9288  nnsub  9344  fzind  9763  uzind4s  9992  uzind4s2  9993  indstr  9995  supinfneg  9997  infsupneg  9998  frec2uzuzd  10841  frec2uzltd  10842  uzsinds  10883  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  seqf1oglem2  10959  seqf1og  10960  seq3id2  10965  seqhomog  10969  expcl2lemap  10990  nn0ltexp2  11149  facdiv  11178  facwordi  11180  zfz1isolem1  11294  zfz1iso  11295  seq3coll  11296  wrdind  11496  wrd2ind  11497  swrdccatin1  11499  swrdccat3blem  11513  reuccatpfxs1lem  11520  caucvgre  11749  fimaxre2  11995  climcn1  12076  climcn2  12077  subcn2  12079  summodclem2a  12150  fsumsplitf  12177  fsum2d  12204  modfsummod  12227  fsumabs  12234  telfsumo  12235  fsumiun  12246  prodfdivap  12316  fprod2d  12392  fproddivapf  12400  fprodsplitf  12401  fprodsplit1f  12403  ndvdssub  12699  bezoutlemmain  12777  bezoutlemex  12780  bezoutlemzz  12781  bezoutlemsup  12788  dfgcd2  12793  algcvg  12828  algcvga  12831  algfx  12832  lcmgcdlem  12857  lcmdvds  12859  coprmgcdb  12868  coprmdvds1  12871  coprmdvds2  12873  prmind2  12900  dvdsprime  12902  nprm  12903  dvdsprm  12917  exprmfct  12918  isprm5lem  12921  coprm  12924  isprm6  12927  prmfac1  12932  sqrt2irr  12942  pcqmul  13084  pcqcl  13087  pc2dvds  13111  pcz  13113  prmpwdvds  13136  ballotfilem2  13230  ennnfonelemim  13317  exmidunben  13319  infpn2  13349  setscomd  13395  mhmlem  13919  isnsg2  14008  ghmf1  14078  islring  14501  lringuplu  14505  opprlring  14506  rrgval  14572  rrgeq0i  14574  isdomn  14580  domneq0  14583  opprdomnbg  14585  znidom  14994  znrrg  14997  mplvalcoe  15083  mplsubgfilemcl  15092  uniopn  15104  fiinopn  15107  epttop  15193  cnpval  15301  iscnp  15302  icnpimaex  15314  lmcvg  15320  cnptoprest  15342  cnptoprest2  15343  lmss  15349  lmff  15352  txcnp  15374  txlm  15382  cnmpt12  15390  cnmpt22  15397  blssps  15530  blss  15531  metss  15597  comet  15602  metcnp3  15614  metcnp2  15616  txmetcnp  15621  divcnap  15668  mpomulcn  15669  elcncf2  15677  cncfi  15681  mulc1cncf  15692  cncfmet  15695  mulcncflem  15710  mulcncf  15711  dedekindeulemloc  15722  dedekindeulemlu  15724  dedekindeulemeu  15725  suplociccreex  15727  dedekindicclemloc  15731  dedekindicclemlu  15733  dedekindicclemeu  15734  ivthinclemlopn  15739  ivthinclemlr  15740  ivthinclemuopn  15741  ivthinclemur  15742  ivthinclemloc  15744  ivthreinc  15748  limccl  15762  ellimc3apf  15763  limccnpcntop  15778  limccnp2lem  15779  limccoap  15781  dvcoapbr  15810  dvmptfsum  15828  mpodvdsmulf1o  16110  perfectlem2  16120  bcmono  16124  lgsdir2lem4  16162  gausslemma2dlem0i  16188  lgseisenlem2  16202  lgsquad2lem2  16213  2sqlem6  16251  2sqlem8  16254  2sqlem10  16256  gropd  16300  grstructd2dom  16301  upgredg2vtx  16401  upgredgpr  16402  eupth2fi  16732  lealltlt1  16763  lealltlt2  16764  dichmul0orlem7  16771  cbvrald  16828  bj-bdfindes  16987  bj-omtrans  16994  bj-inf2vnlem1  17008  bj-inf2vnlem2  17009  bj-inf2vnlem3  17010  bj-inf2vnlem4  17011  bj-findes  17019  strcoll2  17021  sscoll2  17026  subctctexmid  17042  pw1nct  17045  exmidnotnotr  17048  exmidcon  17049  wexmiddiffilem  17055  wexmiddifxy  17058  exmidsbthrlem  17079  sbthom  17083  apdiff  17109  ismkvnnlem  17114  nconstwlpolem  17127  neapmkv  17130  neap0mkv  17131  ltlenmkv  17132  alsbid  17155  cbvals  17158