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  818  nfbidf  1520  drnf1  1712  drnf2  1713  equveli  1733  ax11v2  1793  ax11v  1800  ax11ev  1801  equs5or  1803  mobidh  2034  mobid  2035  axext3  2123  cbvralf  2651  cbvraldva2  2664  gencbval  2737  vtoclgaf  2754  vtocl2gaf  2756  vtocl3gaf  2758  rspct  2786  rspc  2787  rspc2gv  2805  ceqex  2816  ralab2  2852  mob2  2868  mob  2870  morex  2872  reu7  2883  reu8  2884  nelrdva  2895  cdeqim  2906  sbcimg  2954  csbhypf  3043  cbvralcsf  3067  dfss2f  3093  sbcssg  3477  sneqrg  3697  elintab  3790  intss1  3794  intmin  3799  dfiin2g  3854  disji2  3930  disjiun  3932  trel  4041  trss  4043  bnd2  4105  zfpow  4107  exmidexmid  4128  exmidsssnc  4134  exmidundifim  4138  rext  4145  opth  4167  copsexg  4174  poeq1  4229  pocl  4233  swopolem  4235  swopo  4236  soeq1  4245  sowlin  4250  frforeq2  4275  frforeq3  4277  frirrg  4280  frind  4282  weeq1  4286  ordelord  4311  reusv3i  4388  ordtriexmid  4445  ontr2exmid  4448  onsucsssucexmid  4450  onsucelsucexmid  4453  ordsucunielexmid  4454  regexmidlem1  4456  regexmid  4458  reg2exmid  4459  elirr  4464  en2lp  4477  ordsoexmid  4485  onintexmid  4495  reg3exmid  4502  tfis  4505  tfisi  4509  peano2  4517  findes  4525  nnregexmid  4542  omsinds  4543  vtoclr  4595  poinxp  4616  soinxp  4617  posng  4619  ssrel  4635  ssrel2  4637  ssrelrel  4647  relop  4697  issref  4929  iota5  5116  dffun4f  5147  sbcfung  5155  funopg  5165  brprcneu  5422  funfveu  5442  tz6.12f  5458  funbrfv  5468  ssimaexg  5491  fvmptss2  5504  fvmptssdm  5513  fvmptf  5521  fvelrn  5559  f1veqaeq  5678  dff13f  5679  isopolem  5731  isosolem  5733  riota5f  5762  imbrov2fvoveq  5807  oprabid  5811  ovmpos  5902  ov2gf  5903  ovi3  5915  caovcan  5943  caovordig  5944  caofrss  6014  caoftrn  6015  dfoprab4f  6099  f1o2ndf1  6133  poxp  6137  smoel  6205  tfrlem1  6213  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  nnsucelsuc  6395  nnsucsssuc  6396  nnmordi  6420  nnaordex  6431  qsel  6514  eroveu  6528  ecopovtrn  6534  ecopovtrng  6537  th3qlem2  6540  ixpsnf1o  6638  fundmeng  6709  phplem3g  6758  nneneq  6759  ssfiexmid  6778  domfiexmid  6780  findcard  6790  findcard2  6791  findcard2s  6792  findcard2d  6793  findcard2sd  6794  diffifi  6796  ac6sfi  6800  fiintim  6825  fisseneq  6828  fidcenumlemrk  6850  fidcenumlemr  6851  isbth  6863  supeq3  6885  supeq123d  6886  supmoti  6888  suplubti  6895  supisolem  6903  cnvinfex  6913  eqinfti  6915  infvalti  6917  ordiso2  6928  isomni  7016  finomni  7020  exmidomni  7022  ctssexmid  7032  ismkv  7035  ismkvnex  7037  mkvprop  7040  fodjumkvlemres  7041  enmkvlem  7043  iswomni  7047  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  ccfunen  7096  ltsonq  7230  ltexnqq  7240  prcdnql  7316  prcunqu  7317  prloc  7323  prdisj  7324  genprndl  7353  genprndu  7354  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemcl  7508  caucvgprprlemcbv  7519  caucvgprprlemval  7520  suplocexprlemloc  7553  lttrsr  7594  ltsosr  7596  recexgt0sr  7605  mulgt0sr  7610  aptisr  7611  mulextsr1  7613  srpospr  7615  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  caucvgsr  7634  map2psrprg  7637  suplocsrlemb  7638  axprecex  7712  axpre-ltwlin  7715  axpre-lttrn  7716  axpre-apti  7717  axpre-mulgt0  7719  axpre-mulext  7720  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  axsuploc  7861  ltleletr  7870  ltordlem  8268  squeeze0  8686  sup3exmid  8739  nnsub  8783  fzind  9190  uzind4s  9412  uzind4s2  9413  indstr  9415  supinfneg  9417  infsupneg  9418  frec2uzuzd  10206  frec2uzltd  10207  uzsinds  10246  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  seq3id2  10313  expcl2lemap  10336  facdiv  10516  facwordi  10518  zfz1isolem1  10615  zfz1iso  10616  seq3coll  10617  caucvgre  10785  fimaxre2  11030  climcn1  11109  climcn2  11110  subcn2  11112  summodclem2a  11182  fsumsplitf  11209  fsum2d  11236  modfsummod  11259  fsumabs  11266  telfsumo  11267  fsumiun  11278  prodfdivap  11348  ndvdssub  11663  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemsup  11733  dfgcd2  11738  algcvg  11765  algcvga  11768  algfx  11769  lcmgcdlem  11794  lcmdvds  11796  coprmgcdb  11805  coprmdvds1  11808  coprmdvds2  11810  prmind2  11837  dvdsprime  11839  nprm  11840  dvdsprm  11853  exprmfct  11854  coprm  11858  isprm6  11861  prmfac1  11866  sqrt2irr  11876  ennnfonelemim  11973  exmidunben  11975  uniopn  12207  fiinopn  12210  epttop  12298  cnpval  12406  iscnp  12407  icnpimaex  12419  lmcvg  12425  cnptoprest  12447  cnptoprest2  12448  lmss  12454  lmff  12457  txcnp  12479  txlm  12487  cnmpt12  12495  cnmpt22  12502  blssps  12635  blss  12636  metss  12702  comet  12707  metcnp3  12719  metcnp2  12721  txmetcnp  12726  divcnap  12763  elcncf2  12769  cncfi  12773  mulc1cncf  12784  cncfmet  12787  mulcncflem  12798  mulcncf  12799  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeulemeu  12808  suplociccreex  12810  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemeu  12817  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  limccl  12836  ellimc3apf  12837  limccnpcntop  12852  limccnp2lem  12853  limccoap  12855  dvcoapbr  12879  cbvrald  13166  bj-bdfindes  13318  bj-omtrans  13325  bj-inf2vnlem1  13339  bj-inf2vnlem2  13340  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342  bj-findes  13350  strcoll2  13352  sscoll2  13357  exmid1stab  13368  subctctexmid  13369  pw1nct  13371  exmidsbthrlem  13392  sbthom  13396  apdiff  13416  ismkvnnlem  13419  neapmkv  13425