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  832  nfbidf  1539  drnf1  1733  drnf2  1734  equveli  1759  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  mobidh  2060  mobid  2061  axext3  2160  cbvralfw  2695  cbvralf  2697  cbvralvw  2709  cbvraldva2  2712  gencbval  2787  vtoclgaf  2804  vtocl2gaf  2806  vtocl3gaf  2808  rspct  2836  rspc  2837  rspc2gv  2855  ceqex  2866  ralab2  2903  mob2  2919  mob  2921  morex  2923  reu7  2934  reu8  2935  nelrdva  2946  cdeqim  2957  sbcimg  3006  csbhypf  3097  cbvralcsf  3121  dfss2f  3148  sbcssg  3534  sneqrg  3764  elintab  3857  intss1  3861  intmin  3866  dfiin2g  3921  disji2  3998  disjiun  4000  trel  4110  trss  4112  bnd2  4175  zfpow  4177  exmidexmid  4198  exmidsssnc  4205  exmidundifim  4209  exmid1stab  4210  rext  4217  opth  4239  copsexg  4246  poeq1  4301  pocl  4305  swopolem  4307  swopo  4308  soeq1  4317  sowlin  4322  frforeq2  4347  frforeq3  4349  frirrg  4352  frind  4354  weeq1  4358  ordelord  4383  reusv3i  4461  ordtriexmid  4522  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmid  4531  ordsucunielexmid  4532  regexmidlem1  4534  regexmid  4536  reg2exmid  4537  elirr  4542  en2lp  4555  ordsoexmid  4563  onintexmid  4574  reg3exmid  4581  tfis  4584  tfisi  4588  peano2  4596  findes  4604  nnregexmid  4622  omsinds  4623  vtoclr  4676  poinxp  4697  soinxp  4698  posng  4700  ssrel  4716  ssrel2  4718  ssrelrel  4728  relop  4779  issref  5013  iota5  5200  dffun4f  5234  sbcfung  5242  funopg  5252  brprcneu  5510  funfveu  5530  tz6.12f  5546  funbrfv  5556  ssimaexg  5580  fvmptss2  5593  fvmptssdm  5602  fvmptf  5610  fvelrn  5649  f1veqaeq  5772  dff13f  5773  isopolem  5825  isosolem  5827  riota5f  5857  imbrov2fvoveq  5902  oprabid  5909  ovmpos  6000  ov2gf  6001  ovi3  6013  caovcan  6041  caovordig  6042  caofrss  6109  caoftrn  6110  dfoprab4f  6196  f1o2ndf1  6231  poxp  6235  smoel  6303  tfrlem1  6311  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  nnsucelsuc  6494  nnsucsssuc  6495  nnmordi  6519  nnaordex  6531  qsel  6614  eroveu  6628  ecopovtrn  6634  ecopovtrng  6637  th3qlem2  6640  ixpsnf1o  6738  fundmeng  6809  phplem3g  6858  nneneq  6859  ssfiexmid  6878  domfiexmid  6880  findcard  6890  findcard2  6891  findcard2s  6892  findcard2d  6893  findcard2sd  6894  diffifi  6896  ac6sfi  6900  fiintim  6930  fisseneq  6933  fidcenumlemrk  6955  fidcenumlemr  6956  isbth  6968  supeq3  6991  supeq123d  6992  supmoti  6994  suplubti  7001  supisolem  7009  cnvinfex  7019  eqinfti  7021  infvalti  7023  ordiso2  7036  nnnninfeq2  7129  isomni  7136  finomni  7140  exmidomni  7142  ctssexmid  7150  ismkv  7153  ismkvnex  7155  mkvprop  7158  fodjumkvlemres  7159  enmkvlem  7161  iswomni  7165  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  tapeq1  7253  exmidapne  7261  ccfunen  7265  ltsonq  7399  ltexnqq  7409  prcdnql  7485  prcunqu  7486  prloc  7492  prdisj  7493  genprndl  7522  genprndu  7523  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemcl  7677  caucvgprprlemcbv  7688  caucvgprprlemval  7689  suplocexprlemloc  7722  lttrsr  7763  ltsosr  7765  recexgt0sr  7774  mulgt0sr  7779  aptisr  7780  mulextsr1  7782  srpospr  7784  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  caucvgsr  7803  map2psrprg  7806  suplocsrlemb  7807  axprecex  7881  axpre-ltwlin  7884  axpre-lttrn  7885  axpre-apti  7886  axpre-mulgt0  7888  axpre-mulext  7889  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  axsuploc  8032  ltleletr  8041  ltordlem  8441  squeeze0  8863  sup3exmid  8916  nnsub  8960  fzind  9370  uzind4s  9592  uzind4s2  9593  indstr  9595  supinfneg  9597  infsupneg  9598  frec2uzuzd  10404  frec2uzltd  10405  uzsinds  10444  seq3fveq2  10471  seq3shft2  10475  monoord  10478  seq3split  10481  seq3id2  10511  expcl2lemap  10534  nn0ltexp2  10691  facdiv  10720  facwordi  10722  zfz1isolem1  10822  zfz1iso  10823  seq3coll  10824  caucvgre  10992  fimaxre2  11237  climcn1  11318  climcn2  11319  subcn2  11321  summodclem2a  11391  fsumsplitf  11418  fsum2d  11445  modfsummod  11468  fsumabs  11475  telfsumo  11476  fsumiun  11487  prodfdivap  11557  fprod2d  11633  fproddivapf  11641  fprodsplitf  11642  fprodsplit1f  11644  ndvdssub  11937  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemzz  12005  bezoutlemsup  12012  dfgcd2  12017  algcvg  12050  algcvga  12053  algfx  12054  lcmgcdlem  12079  lcmdvds  12081  coprmgcdb  12090  coprmdvds1  12093  coprmdvds2  12095  prmind2  12122  dvdsprime  12124  nprm  12125  dvdsprm  12139  exprmfct  12140  isprm5lem  12143  coprm  12146  isprm6  12149  prmfac1  12154  sqrt2irr  12164  pcqmul  12305  pcqcl  12308  pc2dvds  12331  pcz  12333  prmpwdvds  12355  ennnfonelemim  12427  exmidunben  12429  infpn2  12459  setscomd  12505  mhmlem  12983  isnsg2  13068  islring  13338  lringuplu  13342  uniopn  13586  fiinopn  13589  epttop  13675  cnpval  13783  iscnp  13784  icnpimaex  13796  lmcvg  13802  cnptoprest  13824  cnptoprest2  13825  lmss  13831  lmff  13834  txcnp  13856  txlm  13864  cnmpt12  13872  cnmpt22  13879  blssps  14012  blss  14013  metss  14079  comet  14084  metcnp3  14096  metcnp2  14098  txmetcnp  14103  divcnap  14140  elcncf2  14146  cncfi  14150  mulc1cncf  14161  cncfmet  14164  mulcncflem  14175  mulcncf  14176  dedekindeulemloc  14182  dedekindeulemlu  14184  dedekindeulemeu  14185  suplociccreex  14187  dedekindicclemloc  14191  dedekindicclemlu  14193  dedekindicclemeu  14194  ivthinclemlopn  14199  ivthinclemlr  14200  ivthinclemuopn  14201  ivthinclemur  14202  ivthinclemloc  14204  limccl  14213  ellimc3apf  14214  limccnpcntop  14229  limccnp2lem  14230  limccoap  14232  dvcoapbr  14256  lgsdir2lem4  14517  lgseisenlem2  14536  2sqlem6  14552  2sqlem8  14555  2sqlem10  14557  cbvrald  14625  bj-bdfindes  14786  bj-omtrans  14793  bj-inf2vnlem1  14807  bj-inf2vnlem2  14808  bj-inf2vnlem3  14809  bj-inf2vnlem4  14810  bj-findes  14818  strcoll2  14820  sscoll2  14825  subctctexmid  14835  pw1nct  14837  exmidsbthrlem  14855  sbthom  14859  apdiff  14881  ismkvnnlem  14885  nconstwlpolem  14898  neapmkv  14901  neap0mkv  14902  ltlenmkv  14903