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  7331  supeq123d  7332  supmoti  7334  suplubti  7341  supisolem  7349  cnvinfex  7359  eqinfti  7361  infvalti  7363  ordiso2  7376  nninfninc  7464  nnnninfeq2  7470  isomni  7477  finomni  7481  exmidomni  7483  ctssexmid  7491  ismkv  7494  ismkvnex  7496  mkvprop  7499  fodjumkvlemres  7500  enmkvlem  7502  iswomni  7506  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  papeq1  7610  papsym  7613  papcotr  7614  tapeq1  7619  exmidapne  7627  ccfunen  7631  ltsonq  7766  ltexnqq  7776  prcdnql  7852  prcunqu  7853  prloc  7859  prdisj  7860  genprndl  7889  genprndu  7890  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemcl  8044  caucvgprprlemcbv  8055  caucvgprprlemval  8056  suplocexprlemloc  8089  lttrsr  8130  ltsosr  8132  recexgt0sr  8141  mulgt0sr  8146  aptisr  8147  mulextsr1  8149  srpospr  8151  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  map2psrprg  8173  suplocsrlemb  8174  axprecex  8248  axpre-ltwlin  8251  axpre-lttrn  8252  axpre-apti  8253  axpre-mulgt0  8255  axpre-mulext  8256  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  axsuploc  8399  ltleletr  8408  ltordlem  8812  squeeze0  9237  sup3exmid  9290  nnsub  9346  fzind  9766  uzind4s  10000  uzind4s2  10001  indstr  10003  supinfneg  10005  infsupneg  10006  frec2uzuzd  10854  frec2uzltd  10855  uzsinds  10896  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seqf1oglem2  10972  seqf1og  10973  seq3id2  10978  seqhomog  10982  expcl2lemap  11003  nn0ltexp2  11163  facdiv  11192  facwordi  11194  zfz1isolem1  11308  zfz1iso  11309  seq3coll  11310  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  swrdccat3blem  11527  reuccatpfxs1lem  11534  caucvgre  11763  fimaxre2  12010  climcn1  12093  climcn2  12094  subcn2  12096  summodclem2a  12167  fsumsplitf  12194  fsum2d  12221  modfsummod  12244  fsumabs  12251  telfsumo  12252  fsumiun  12263  prodfdivap  12333  fprod2d  12409  fproddivapf  12417  fprodsplitf  12418  fprodsplit1f  12420  ndvdssub  12716  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemzz  12798  bezoutlemsup  12805  dfgcd2  12810  algcvg  12845  algcvga  12848  algfx  12849  lcmgcdlem  12874  lcmdvds  12876  coprmgcdb  12885  coprmdvds1  12888  coprmdvds2  12890  prmind2  12917  dvdsprime  12919  nprm  12920  dvdsprm  12935  exprmfct  12936  isprm5lem  12939  coprm  12942  isprm6  12945  prmfac1  12950  sqrt2irr  12960  pcqmul  13105  pcqcl  13108  pc2dvds  13132  pcz  13134  prmpwdvds  13157  prmlem0  13243  ballotfilem2  13280  ennnfonelemim  13367  exmidunben  13369  infpn2  13399  setscomd  13445  mhmlem  13969  isnsg2  14058  ghmf1  14128  islring  14551  lringuplu  14555  opprlring  14556  rrgval  14622  rrgeq0i  14624  isdomn  14630  domneq0  14633  opprdomnbg  14635  znidom  15044  znrrg  15047  mplvalcoe  15140  mplsubgfilemcl  15149  uniopn  15161  fiinopn  15164  epttop  15250  cnpval  15358  iscnp  15359  icnpimaex  15371  lmcvg  15377  cnptoprest  15399  cnptoprest2  15400  lmss  15406  lmff  15409  txcnp  15431  txlm  15439  cnmpt12  15447  cnmpt22  15454  blssps  15587  blss  15588  metss  15654  comet  15659  metcnp3  15671  metcnp2  15673  txmetcnp  15678  divcnap  15725  mpomulcn  15726  elcncf2  15734  cncfi  15738  mulc1cncf  15749  cncfmet  15752  mulcncflem  15767  mulcncf  15768  dedekindeulemloc  15779  dedekindeulemlu  15781  dedekindeulemeu  15782  suplociccreex  15784  dedekindicclemloc  15788  dedekindicclemlu  15790  dedekindicclemeu  15791  ivthinclemlopn  15796  ivthinclemlr  15797  ivthinclemuopn  15798  ivthinclemur  15799  ivthinclemloc  15801  ivthreinc  15805  limccl  15819  ellimc3apf  15820  limccnpcntop  15835  limccnp2lem  15836  limccoap  15838  dvcoapbr  15867  dvmptfsum  15885  mpodvdsmulf1o  16213  perfectlem2  16229  bcmono  16233  lgsdir2lem4  16284  gausslemma2dlem0i  16310  lgseisenlem2  16324  lgsquad2lem2  16335  2sqlem6  16373  2sqlem8  16376  2sqlem10  16378  gropd  16422  grstructd2dom  16423  upgredg2vtx  16523  upgredgpr  16524  eupth2fi  16854  lealltlt1  16885  lealltlt2  16886  dichmul0orlem7  16893  cbvrald  16950  bj-bdfindes  17109  bj-omtrans  17116  bj-inf2vnlem1  17130  bj-inf2vnlem2  17131  bj-inf2vnlem3  17132  bj-inf2vnlem4  17133  bj-findes  17141  strcoll2  17143  sscoll2  17148  subctctexmid  17164  pw1nct  17167  exmidnotnotr  17170  exmidcon  17171  wexmiddiffilem  17177  wexmiddifxy  17180  exmidsbthrlem  17201  sbthom  17205  apdiff  17231  ismkvnnlem  17236  nconstwlpolem  17249  neapmkv  17252  neap0mkv  17253  ltlenmkv  17254  alsbid  17277  cbvals  17280