Theorem imbi12d 233

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 230	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 229	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  817  nfbidf  1519  drnf1  1711  drnf2  1712  equveli  1732  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  mobidh  2033  mobid  2034  axext3  2122  cbvralf  2648  cbvraldva2  2661  gencbval  2734  vtoclgaf  2751  vtocl2gaf  2753  vtocl3gaf  2755  rspct  2782  rspc  2783  rspc2gv  2801  ceqex  2812  ralab2  2848  mob2  2864  mob  2866  morex  2868  reu7  2879  reu8  2880  nelrdva  2891  cdeqim  2902  sbcimg  2950  csbhypf  3038  cbvralcsf  3062  dfss2f  3088  sbcssg  3472  sneqrg  3689  elintab  3782  intss1  3786  intmin  3791  dfiin2g  3846  disji2  3922  disjiun  3924  trel  4033  trss  4035  bnd2  4097  zfpow  4099  exmidexmid  4120  exmidsssnc  4126  exmidundifim  4130  rext  4137  opth  4159  copsexg  4166  poeq1  4221  pocl  4225  swopolem  4227  swopo  4228  soeq1  4237  sowlin  4242  frforeq2  4267  frforeq3  4269  frirrg  4272  frind  4274  weeq1  4278  ordelord  4303  reusv3i  4380  ordtriexmid  4437  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  ordsucunielexmid  4446  regexmidlem1  4448  regexmid  4450  reg2exmid  4451  elirr  4456  en2lp  4469  ordsoexmid  4477  onintexmid  4487  reg3exmid  4494  tfis  4497  tfisi  4501  peano2  4509  findes  4517  nnregexmid  4534  omsinds  4535  vtoclr  4587  poinxp  4608  soinxp  4609  posng  4611  ssrel  4627  ssrel2  4629  ssrelrel  4639  relop  4689  issref  4921  iota5  5108  dffun4f  5139  sbcfung  5147  funopg  5157  brprcneu  5414  funfveu  5434  tz6.12f  5450  funbrfv  5460  ssimaexg  5483  fvmptss2  5496  fvmptssdm  5505  fvmptf  5513  fvelrn  5551  f1veqaeq  5670  dff13f  5671  isopolem  5723  isosolem  5725  riota5f  5754  imbrov2fvoveq  5799  oprabid  5803  ovmpos  5894  ov2gf  5895  ovi3  5907  caovcan  5935  caovordig  5936  caofrss  6006  caoftrn  6007  dfoprab4f  6091  f1o2ndf1  6125  poxp  6129  smoel  6197  tfrlem1  6205  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  nnsucelsuc  6387  nnsucsssuc  6388  nnmordi  6412  nnaordex  6423  qsel  6506  eroveu  6520  ecopovtrn  6526  ecopovtrng  6529  th3qlem2  6532  ixpsnf1o  6630  fundmeng  6701  phplem3g  6750  nneneq  6751  ssfiexmid  6770  domfiexmid  6772  findcard  6782  findcard2  6783  findcard2s  6784  findcard2d  6785  findcard2sd  6786  diffifi  6788  ac6sfi  6792  fiintim  6817  fisseneq  6820  fidcenumlemrk  6842  fidcenumlemr  6843  isbth  6855  supeq3  6877  supeq123d  6878  supmoti  6880  suplubti  6887  supisolem  6895  cnvinfex  6905  eqinfti  6907  infvalti  6909  ordiso2  6920  isomni  7008  finomni  7012  exmidomni  7014  ctssexmid  7024  ismkv  7027  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  ccfunen  7079  ltsonq  7206  ltexnqq  7216  prcdnql  7292  prcunqu  7293  prloc  7299  prdisj  7300  genprndl  7329  genprndu  7330  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemcl  7484  caucvgprprlemcbv  7495  caucvgprprlemval  7496  suplocexprlemloc  7529  lttrsr  7570  ltsosr  7572  recexgt0sr  7581  mulgt0sr  7586  aptisr  7587  mulextsr1  7589  srpospr  7591  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  caucvgsr  7610  map2psrprg  7613  suplocsrlemb  7614  axprecex  7688  axpre-ltwlin  7691  axpre-lttrn  7692  axpre-apti  7693  axpre-mulgt0  7695  axpre-mulext  7696  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  axsuploc  7837  ltleletr  7846  ltordlem  8244  squeeze0  8662  sup3exmid  8715  nnsub  8759  fzind  9166  uzind4s  9385  uzind4s2  9386  indstr  9388  supinfneg  9390  infsupneg  9391  frec2uzuzd  10175  frec2uzltd  10176  uzsinds  10215  seq3fveq2  10242  seq3shft2  10246  monoord  10249  seq3split  10252  seq3id2  10282  expcl2lemap  10305  facdiv  10484  facwordi  10486  zfz1isolem1  10583  zfz1iso  10584  seq3coll  10585  caucvgre  10753  fimaxre2  10998  climcn1  11077  climcn2  11078  subcn2  11080  summodclem2a  11150  fsumsplitf  11177  fsum2d  11204  modfsummod  11227  fsumabs  11234  telfsumo  11235  fsumiun  11246  prodfdivap  11316  ndvdssub  11627  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemzz  11690  bezoutlemsup  11697  dfgcd2  11702  algcvg  11729  algcvga  11732  algfx  11733  lcmgcdlem  11758  lcmdvds  11760  coprmgcdb  11769  coprmdvds1  11772  coprmdvds2  11774  prmind2  11801  dvdsprime  11803  nprm  11804  dvdsprm  11817  exprmfct  11818  coprm  11822  isprm6  11825  prmfac1  11830  sqrt2irr  11840  ennnfonelemim  11937  exmidunben  11939  uniopn  12168  fiinopn  12171  epttop  12259  cnpval  12367  iscnp  12368  icnpimaex  12380  lmcvg  12386  cnptoprest  12408  cnptoprest2  12409  lmss  12415  lmff  12418  txcnp  12440  txlm  12448  cnmpt12  12456  cnmpt22  12463  blssps  12596  blss  12597  metss  12663  comet  12668  metcnp3  12680  metcnp2  12682  txmetcnp  12687  divcnap  12724  elcncf2  12730  cncfi  12734  mulc1cncf  12745  cncfmet  12748  mulcncflem  12759  mulcncf  12760  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeulemeu  12769  suplociccreex  12771  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemeu  12778  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  limccl  12797  ellimc3apf  12798  limccnpcntop  12813  limccnp2lem  12814  limccoap  12816  dvcoapbr  12840  cbvrald  12995  bj-bdfindes  13147  bj-omtrans  13154  bj-inf2vnlem1  13168  bj-inf2vnlem2  13169  bj-inf2vnlem3  13170  bj-inf2vnlem4  13171  bj-findes  13179  strcoll2  13181  sscoll2  13186  exmid1stab  13195  subctctexmid  13196  exmidsbthrlem  13217  sbthom  13221