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  4238  trss  4240  bnd2  4312  zfpow  4314  exmidexmid  4335  exmidsssnc  4342  exmidundifim  4346  exmid1stab  4347  rext  4357  opth  4379  copsexg  4386  poeq1  4446  pocl  4450  swopolem  4452  swopo  4453  soeq1  4462  sowlin  4467  frforeq2  4492  frforeq3  4494  frirrg  4497  frind  4499  weeq1  4503  ordelord  4528  reusv3i  4607  ordtriexmid  4670  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  ordsucunielexmid  4680  regexmidlem1  4682  regexmid  4684  reg2exmid  4685  elirr  4690  en2lp  4703  ordsoexmid  4711  onintexmid  4722  reg3exmid  4729  tfis  4732  tfisi  4736  peano2  4744  findes  4752  nnregexmid  4770  omsinds  4771  vtoclr  4825  poinxp  4846  soinxp  4847  posng  4849  ssrel  4865  ssrel2  4867  ssrelrel  4877  relop  4932  issref  5173  iotaexab  5359  iota5  5362  dffun4f  5396  sbcfung  5404  funopg  5414  brprcneu  5691  funfveu  5711  tz6.12f  5727  funbrfv  5742  ssimaexg  5768  fvmptss2  5783  fvmptssdm  5793  fvmptf  5801  fvelrn  5842  f1veqaeq  5978  dff13f  5979  isopolem  6031  isosolem  6033  riota5f  6068  imbrov2fvoveq  6113  oprabid  6120  ovmpos  6215  ov2gf  6216  ovi3  6229  caovcan  6257  caovordig  6258  caofrss  6338  caoftrn  6339  dfoprab4f  6431  f1o2ndf1  6468  poxp  6472  suppfnss  6501  smoel  6576  tfrlem1  6584  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  nnsucelsuc  6769  nnsucsssuc  6770  nnmordi  6794  nnaordex  6806  qsel  6891  eroveu  6905  ecopovtrn  6911  ecopovtrng  6914  th3qlem2  6917  ixpsnf1o  7024  fundmeng  7101  modom  7114  phplem3g  7163  nneneq  7164  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  findcard  7198  findcard2  7199  findcard2s  7200  findcard2d  7201  findcard2sd  7202  diffifi  7204  ac6sfi  7208  fiintim  7244  fisseneq  7248  fidcenumlemrk  7278  fidcenumlemr  7279  isbth  7291  supeq3  7336  supeq123d  7337  supmoti  7339  suplubti  7346  supisolem  7354  cnvinfex  7364  eqinfti  7366  infvalti  7368  ordiso2  7381  nninfninc  7469  nnnninfeq2  7475  isomni  7482  finomni  7486  exmidomni  7488  ctssexmid  7496  ismkv  7499  ismkvnex  7501  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  iswomni  7511  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  papeq1  7615  papsym  7618  papcotr  7619  tapeq1  7624  exmidapne  7632  ccfunen  7636  ltsonq  7771  ltexnqq  7781  prcdnql  7857  prcunqu  7858  prloc  7864  prdisj  7865  genprndl  7894  genprndu  7895  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemcl  8049  caucvgprprlemcbv  8060  caucvgprprlemval  8061  suplocexprlemloc  8094  lttrsr  8135  ltsosr  8137  recexgt0sr  8146  mulgt0sr  8151  aptisr  8152  mulextsr1  8154  srpospr  8156  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  map2psrprg  8178  suplocsrlemb  8179  axprecex  8253  axpre-ltwlin  8256  axpre-lttrn  8257  axpre-apti  8258  axpre-mulgt0  8260  axpre-mulext  8261  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  axsuploc  8404  ltleletr  8413  ltordlem  8817  squeeze0  9242  sup3exmid  9295  nnsub  9352  fzind  9771  uzind4s  10005  uzind4s2  10006  indstr  10008  supinfneg  10010  infsupneg  10011  frec2uzuzd  10859  frec2uzltd  10860  uzsinds  10901  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  seqf1oglem2  10977  seqf1og  10978  seq3id2  10983  seqhomog  10987  expcl2lemap  11008  nn0ltexp2  11168  facdiv  11197  facwordi  11199  zfz1isolem1  11313  zfz1iso  11314  seq3coll  11315  wrdind  11515  wrd2ind  11516  swrdccatin1  11518  swrdccat3blem  11532  reuccatpfxs1lem  11539  caucvgre  11768  fimaxre2  12015  climcn1  12098  climcn2  12099  subcn2  12101  summodclem2a  12172  fsumsplitf  12199  fsum2d  12226  modfsummod  12249  fsumabs  12256  telfsumo  12257  fsumiun  12268  prodfdivap  12338  fprod2d  12414  fproddivapf  12422  fprodsplitf  12423  fprodsplit1f  12425  ndvdssub  12721  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemzz  12803  bezoutlemsup  12810  dfgcd2  12815  algcvg  12850  algcvga  12853  algfx  12854  lcmgcdlem  12879  lcmdvds  12881  coprmgcdb  12890  coprmdvds1  12893  coprmdvds2  12895  prmind2  12922  dvdsprime  12924  nprm  12925  dvdsprm  12940  exprmfct  12941  isprm5lem  12944  coprm  12947  isprm6  12950  prmfac1  12955  sqrt2irr  12965  pcqmul  13110  pcqcl  13113  pc2dvds  13137  pcz  13139  prmpwdvds  13162  prmlem0  13248  ballotfilem2  13285  ennnfonelemim  13372  exmidunben  13374  infpn2  13404  setscomd  13450  mhmlem  13975  isnsg2  14064  ghmf1  14134  islring  14607  lringuplu  14611  opprlring  14612  rrgval  14678  rrgeq0i  14680  isdomn  14686  domneq0  14689  opprdomnbg  14691  znidom  15100  znrrg  15103  uniopn  15244  fiinopn  15247  epttop  15333  cnpval  15441  iscnp  15442  icnpimaex  15454  lmcvg  15460  cnptoprest  15482  cnptoprest2  15483  lmss  15489  lmff  15492  txcnp  15514  txlm  15522  cnmpt12  15530  cnmpt22  15537  blssps  15670  blss  15671  metss  15737  comet  15742  metcnp3  15754  metcnp2  15756  txmetcnp  15761  divcnap  15808  mpomulcn  15809  elcncf2  15817  cncfi  15821  mulc1cncf  15832  cncfmet  15835  mulcncflem  15850  mulcncf  15851  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeulemeu  15865  suplociccreex  15867  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicclemeu  15874  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthreinc  15888  limccl  15902  ellimc3apf  15903  limccnpcntop  15918  limccnp2lem  15919  limccoap  15921  dvcoapbr  15950  dvmptfsum  15968  mpodvdsmulf1o  16301  perfectlem2  16317  bcmono  16321  lgsdir2lem4  16372  gausslemma2dlem0i  16398  lgseisenlem2  16412  lgsquad2lem2  16423  2sqlem6  16461  2sqlem8  16464  2sqlem10  16466  gropd  16510  grstructd2dom  16511  upgredg2vtx  16611  upgredgpr  16612  eupth2fi  16942  lealltlt1  16973  lealltlt2  16974  dichmul0orlem7  16981  cbvrald  17038  bj-bdfindes  17197  bj-omtrans  17204  bj-inf2vnlem1  17218  bj-inf2vnlem2  17219  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221  bj-findes  17229  strcoll2  17231  sscoll2  17236  subctctexmid  17252  pw1nct  17255  exmidnotnotr  17258  exmidcon  17259  wexmiddiffilem  17265  wexmiddifxy  17268  exmidsbthrlem  17290  sbthom  17294  apdiff  17321  ismkvnnlem  17326  nconstwlpolem  17339  neapmkv  17342  neap0mkv  17343  ltlenmkv  17344  alsbid  17367  cbvals  17370