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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  834  nfbidf  1563  drnf1  1757  drnf2  1758  equveli  1783  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  mobidh  2089  mobid  2090  axext3  2189  cbvralfw  2729  cbvralf  2731  cbvralvw  2743  cbvraldva2  2746  gencbval  2823  vtoclgaf  2840  vtocl2gaf  2842  vtocl3gaf  2844  rspct  2872  rspc  2873  rspc2gv  2891  ceqex  2902  ralab2  2939  mob2  2955  mob  2957  morex  2959  reu7  2970  reu8  2971  nelrdva  2982  cdeqim  2993  sbcimg  3042  csbhypf  3134  cbvralcsf  3158  dfss2f  3186  sbcssg  3571  sneqrg  3806  elintab  3899  intss1  3903  intmin  3908  dfiin2g  3963  disji2  4040  disjiun  4043  trel  4154  trss  4156  bnd2  4222  zfpow  4224  exmidexmid  4245  exmidsssnc  4252  exmidundifim  4256  exmid1stab  4257  rext  4264  opth  4286  copsexg  4293  poeq1  4351  pocl  4355  swopolem  4357  swopo  4358  soeq1  4367  sowlin  4372  frforeq2  4397  frforeq3  4399  frirrg  4402  frind  4404  weeq1  4408  ordelord  4433  reusv3i  4511  ordtriexmid  4574  ontr2exmid  4578  onsucsssucexmid  4580  onsucelsucexmid  4583  ordsucunielexmid  4584  regexmidlem1  4586  regexmid  4588  reg2exmid  4589  elirr  4594  en2lp  4607  ordsoexmid  4615  onintexmid  4626  reg3exmid  4633  tfis  4636  tfisi  4640  peano2  4648  findes  4656  nnregexmid  4674  omsinds  4675  vtoclr  4728  poinxp  4749  soinxp  4750  posng  4752  ssrel  4768  ssrel2  4770  ssrelrel  4780  relop  4833  issref  5071  iotaexab  5256  iota5  5259  dffun4f  5293  sbcfung  5301  funopg  5311  brprcneu  5579  funfveu  5599  tz6.12f  5615  funbrfv  5627  ssimaexg  5651  fvmptss2  5664  fvmptssdm  5674  fvmptf  5682  fvelrn  5721  f1veqaeq  5848  dff13f  5849  isopolem  5901  isosolem  5903  riota5f  5934  imbrov2fvoveq  5979  oprabid  5986  ovmpos  6079  ov2gf  6080  ovi3  6093  caovcan  6121  caovordig  6122  caofrss  6200  caoftrn  6201  dfoprab4f  6289  f1o2ndf1  6324  poxp  6328  smoel  6396  tfrlem1  6404  tfr1onlemsucfn  6436  tfr1onlemsucaccv  6437  tfr1onlembxssdm  6439  tfr1onlembfn  6440  tfr1onlemaccex  6444  tfr1onlemres  6445  tfrcllemsucfn  6449  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllembfn  6453  tfrcllemaccex  6457  tfrcllemres  6458  tfrcl  6460  nnsucelsuc  6587  nnsucsssuc  6588  nnmordi  6612  nnaordex  6624  qsel  6709  eroveu  6723  ecopovtrn  6729  ecopovtrng  6732  th3qlem2  6735  ixpsnf1o  6833  fundmeng  6910  phplem3g  6965  nneneq  6966  ssfiexmid  6985  domfiexmid  6987  findcard  6997  findcard2  6998  findcard2s  6999  findcard2d  7000  findcard2sd  7001  diffifi  7003  ac6sfi  7007  fiintim  7040  fisseneq  7043  fidcenumlemrk  7068  fidcenumlemr  7069  isbth  7081  supeq3  7104  supeq123d  7105  supmoti  7107  suplubti  7114  supisolem  7122  cnvinfex  7132  eqinfti  7134  infvalti  7136  ordiso2  7149  nninfninc  7237  nnnninfeq2  7243  isomni  7250  finomni  7254  exmidomni  7256  ctssexmid  7264  ismkv  7267  ismkvnex  7269  mkvprop  7272  fodjumkvlemres  7273  enmkvlem  7275  iswomni  7279  exmidfodomrlemr  7323  exmidfodomrlemrALT  7324  tapeq1  7377  exmidapne  7385  ccfunen  7389  ltsonq  7524  ltexnqq  7534  prcdnql  7610  prcunqu  7611  prloc  7617  prdisj  7618  genprndl  7647  genprndu  7648  caucvgprlemnkj  7792  caucvgprlemnbj  7793  caucvgprlemcl  7802  caucvgprprlemcbv  7813  caucvgprprlemval  7814  suplocexprlemloc  7847  lttrsr  7888  ltsosr  7890  recexgt0sr  7899  mulgt0sr  7904  aptisr  7905  mulextsr1  7907  srpospr  7909  caucvgsrlemgt1  7921  caucvgsrlemoffres  7926  caucvgsr  7928  map2psrprg  7931  suplocsrlemb  7932  axprecex  8006  axpre-ltwlin  8009  axpre-lttrn  8010  axpre-apti  8011  axpre-mulgt0  8013  axpre-mulext  8014  axcaucvglemcau  8024  axcaucvglemres  8025  axpre-suploclemres  8027  axpre-suploc  8028  axsuploc  8158  ltleletr  8167  ltordlem  8568  squeeze0  8990  sup3exmid  9043  nnsub  9088  fzind  9501  uzind4s  9724  uzind4s2  9725  indstr  9727  supinfneg  9729  infsupneg  9730  frec2uzuzd  10560  frec2uzltd  10561  uzsinds  10602  seq3fveq2  10633  seqfveq2g  10635  seq3shft2  10639  seqshft2g  10640  monoord  10643  seq3split  10646  seqsplitg  10647  seqf1oglem2  10678  seqf1og  10679  seq3id2  10684  seqhomog  10688  expcl2lemap  10709  nn0ltexp2  10867  facdiv  10896  facwordi  10898  zfz1isolem1  10998  zfz1iso  10999  seq3coll  11000  caucvgre  11342  fimaxre2  11588  climcn1  11669  climcn2  11670  subcn2  11672  summodclem2a  11742  fsumsplitf  11769  fsum2d  11796  modfsummod  11819  fsumabs  11826  telfsumo  11827  fsumiun  11838  prodfdivap  11908  fprod2d  11984  fproddivapf  11992  fprodsplitf  11993  fprodsplit1f  11995  ndvdssub  12291  bezoutlemmain  12369  bezoutlemex  12372  bezoutlemzz  12373  bezoutlemsup  12380  dfgcd2  12385  algcvg  12420  algcvga  12423  algfx  12424  lcmgcdlem  12449  lcmdvds  12451  coprmgcdb  12460  coprmdvds1  12463  coprmdvds2  12465  prmind2  12492  dvdsprime  12494  nprm  12495  dvdsprm  12509  exprmfct  12510  isprm5lem  12513  coprm  12516  isprm6  12519  prmfac1  12524  sqrt2irr  12534  pcqmul  12676  pcqcl  12679  pc2dvds  12703  pcz  12705  prmpwdvds  12728  ennnfonelemim  12845  exmidunben  12847  infpn2  12877  setscomd  12923  mhmlem  13500  isnsg2  13589  ghmf1  13659  islring  14004  lringuplu  14008  rrgval  14074  rrgeq0i  14076  isdomn  14081  domneq0  14084  opprdomnbg  14086  znidom  14469  znrrg  14472  mplvalcoe  14502  mplsubgfilemcl  14511  uniopn  14523  fiinopn  14526  epttop  14612  cnpval  14720  iscnp  14721  icnpimaex  14733  lmcvg  14739  cnptoprest  14761  cnptoprest2  14762  lmss  14768  lmff  14771  txcnp  14793  txlm  14801  cnmpt12  14809  cnmpt22  14816  blssps  14949  blss  14950  metss  15016  comet  15021  metcnp3  15033  metcnp2  15035  txmetcnp  15040  divcnap  15087  mpomulcn  15088  elcncf2  15096  cncfi  15100  mulc1cncf  15111  cncfmet  15114  mulcncflem  15129  mulcncf  15130  dedekindeulemloc  15141  dedekindeulemlu  15143  dedekindeulemeu  15144  suplociccreex  15146  dedekindicclemloc  15150  dedekindicclemlu  15152  dedekindicclemeu  15153  ivthinclemlopn  15158  ivthinclemlr  15159  ivthinclemuopn  15160  ivthinclemur  15161  ivthinclemloc  15163  ivthreinc  15167  limccl  15181  ellimc3apf  15182  limccnpcntop  15197  limccnp2lem  15198  limccoap  15200  dvcoapbr  15229  dvmptfsum  15247  mpodvdsmulf1o  15512  perfectlem2  15522  lgsdir2lem4  15558  gausslemma2dlem0i  15584  lgseisenlem2  15598  lgsquad2lem2  15609  2sqlem6  15647  2sqlem8  15650  2sqlem10  15652  gropd  15696  grstructd2dom  15697  cbvrald  15838  bj-bdfindes  15999  bj-omtrans  16006  bj-inf2vnlem1  16020  bj-inf2vnlem2  16021  bj-inf2vnlem3  16022  bj-inf2vnlem4  16023  bj-findes  16031  strcoll2  16033  sscoll2  16038  subctctexmid  16052  pw1nct  16055  exmidsbthrlem  16076  sbthom  16080  apdiff  16102  ismkvnnlem  16106  nconstwlpolem  16119  neapmkv  16122  neap0mkv  16123  ltlenmkv  16124