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  6575  tfrlem1  6583  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  nnsucelsuc  6768  nnsucsssuc  6769  nnmordi  6793  nnaordex  6805  qsel  6890  eroveu  6904  ecopovtrn  6910  ecopovtrng  6913  th3qlem2  6916  ixpsnf1o  7022  fundmeng  7099  modom  7112  phplem3g  7161  nneneq  7162  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  findcard  7196  findcard2  7197  findcard2s  7198  findcard2d  7199  findcard2sd  7200  diffifi  7202  ac6sfi  7206  fiintim  7242  fisseneq  7246  fidcenumlemrk  7276  fidcenumlemr  7277  isbth  7289  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  9772  uzind4s  10006  uzind4s2  10007  indstr  10009  supinfneg  10011  infsupneg  10012  frec2uzuzd  10860  frec2uzltd  10861  uzsinds  10902  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seqf1oglem2  10978  seqf1og  10979  seq3id2  10984  seqhomog  10988  expcl2lemap  11009  nn0ltexp2  11169  facdiv  11198  facwordi  11200  zfz1isolem1  11314  zfz1iso  11315  seq3coll  11316  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccat3blem  11533  reuccatpfxs1lem  11540  caucvgre  11769  fimaxre2  12016  climcn1  12099  climcn2  12100  subcn2  12102  summodclem2a  12173  fsumsplitf  12200  fsum2d  12227  modfsummod  12250  fsumabs  12257  telfsumo  12258  fsumiun  12269  prodfdivap  12339  fprod2d  12415  fproddivapf  12423  fprodsplitf  12424  fprodsplit1f  12426  ndvdssub  12722  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemsup  12811  dfgcd2  12816  algcvg  12851  algcvga  12854  algfx  12855  lcmgcdlem  12880  lcmdvds  12882  coprmgcdb  12891  coprmdvds1  12894  coprmdvds2  12896  prmind2  12923  dvdsprime  12925  nprm  12926  dvdsprm  12941  exprmfct  12942  isprm5lem  12945  coprm  12948  isprm6  12951  prmfac1  12956  sqrt2irr  12966  pcqmul  13111  pcqcl  13114  pc2dvds  13138  pcz  13140  prmpwdvds  13163  prmlem0  13249  ballotfilem2  13286  ennnfonelemim  13373  exmidunben  13375  infpn2  13405  setscomd  13451  mhmlem  13976  isnsg2  14065  ghmf1  14135  islring  14608  lringuplu  14612  opprlring  14613  rrgval  14679  rrgeq0i  14681  isdomn  14687  domneq0  14690  opprdomnbg  14692  znidom  15101  znrrg  15104  mplvalcoe  15206  mplsubgfilemcl  15215  uniopn  15227  fiinopn  15230  epttop  15316  cnpval  15424  iscnp  15425  icnpimaex  15437  lmcvg  15443  cnptoprest  15465  cnptoprest2  15466  lmss  15472  lmff  15475  txcnp  15497  txlm  15505  cnmpt12  15513  cnmpt22  15520  blssps  15653  blss  15654  metss  15720  comet  15725  metcnp3  15737  metcnp2  15739  txmetcnp  15744  divcnap  15791  mpomulcn  15792  elcncf2  15800  cncfi  15804  mulc1cncf  15815  cncfmet  15818  mulcncflem  15833  mulcncf  15834  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeulemeu  15848  suplociccreex  15850  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicclemeu  15857  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthreinc  15871  limccl  15885  ellimc3apf  15886  limccnpcntop  15901  limccnp2lem  15902  limccoap  15904  dvcoapbr  15933  dvmptfsum  15951  mpodvdsmulf1o  16284  perfectlem2  16300  bcmono  16304  lgsdir2lem4  16355  gausslemma2dlem0i  16381  lgseisenlem2  16395  lgsquad2lem2  16406  2sqlem6  16444  2sqlem8  16447  2sqlem10  16449  gropd  16493  grstructd2dom  16494  upgredg2vtx  16594  upgredgpr  16595  eupth2fi  16925  lealltlt1  16956  lealltlt2  16957  dichmul0orlem7  16964  cbvrald  17021  bj-bdfindes  17180  bj-omtrans  17187  bj-inf2vnlem1  17201  bj-inf2vnlem2  17202  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204  bj-findes  17212  strcoll2  17214  sscoll2  17219  subctctexmid  17235  pw1nct  17238  exmidnotnotr  17241  exmidcon  17242  wexmiddiffilem  17248  wexmiddifxy  17251  exmidsbthrlem  17273  sbthom  17277  apdiff  17304  ismkvnnlem  17309  nconstwlpolem  17322  neapmkv  17325  neap0mkv  17326  ltlenmkv  17327  alsbid  17350  cbvals  17353