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  837  nfbidf  1585  drnf1  1779  drnf2  1780  equveli  1805  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  mobidh  2111  mobid  2112  axext3  2212  cbvralfw  2754  cbvralf  2756  cbvralvw  2769  cbvraldva2  2772  gencbval  2849  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspc2gv  2919  ceqex  2930  ralab2  2967  mob2  2983  mob  2985  morex  2987  reu7  2998  reu8  2999  nelrdva  3010  cdeqim  3021  sbcimg  3070  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  sbcssg  3600  sneqrg  3840  elintab  3934  intss1  3938  intmin  3943  dfiin2g  3998  disji2  4075  disjiun  4078  trel  4189  trss  4191  bnd2  4258  zfpow  4260  exmidexmid  4281  exmidsssnc  4288  exmidundifim  4292  exmid1stab  4293  rext  4302  opth  4324  copsexg  4331  poeq1  4391  pocl  4395  swopolem  4397  swopo  4398  soeq1  4407  sowlin  4412  frforeq2  4437  frforeq3  4439  frirrg  4442  frind  4444  weeq1  4448  ordelord  4473  reusv3i  4551  ordtriexmid  4614  ontr2exmid  4618  onsucsssucexmid  4620  onsucelsucexmid  4623  ordsucunielexmid  4624  regexmidlem1  4626  regexmid  4628  reg2exmid  4629  elirr  4634  en2lp  4647  ordsoexmid  4655  onintexmid  4666  reg3exmid  4673  tfis  4676  tfisi  4680  peano2  4688  findes  4696  nnregexmid  4714  omsinds  4715  vtoclr  4769  poinxp  4790  soinxp  4791  posng  4793  ssrel  4809  ssrel2  4811  ssrelrel  4821  relop  4875  issref  5114  iotaexab  5300  iota5  5303  dffun4f  5337  sbcfung  5345  funopg  5355  brprcneu  5625  funfveu  5645  tz6.12f  5661  funbrfv  5675  ssimaexg  5701  fvmptss2  5714  fvmptssdm  5724  fvmptf  5732  fvelrn  5771  f1veqaeq  5902  dff13f  5903  isopolem  5955  isosolem  5957  riota5f  5990  imbrov2fvoveq  6035  oprabid  6042  ovmpos  6137  ov2gf  6138  ovi3  6151  caovcan  6179  caovordig  6180  caofrss  6259  caoftrn  6260  dfoprab4f  6348  f1o2ndf1  6385  poxp  6389  smoel  6457  tfrlem1  6465  tfr1onlemsucfn  6497  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemaccex  6505  tfr1onlemres  6506  tfrcllemsucfn  6510  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemaccex  6518  tfrcllemres  6519  tfrcl  6521  nnsucelsuc  6650  nnsucsssuc  6651  nnmordi  6675  nnaordex  6687  qsel  6772  eroveu  6786  ecopovtrn  6792  ecopovtrng  6795  th3qlem2  6798  ixpsnf1o  6896  fundmeng  6973  phplem3g  7030  nneneq  7031  ssfiexmid  7051  domfiexmid  7053  findcard  7063  findcard2  7064  findcard2s  7065  findcard2d  7066  findcard2sd  7067  diffifi  7069  ac6sfi  7073  fiintim  7109  fisseneq  7112  fidcenumlemrk  7137  fidcenumlemr  7138  isbth  7150  supeq3  7173  supeq123d  7174  supmoti  7176  suplubti  7183  supisolem  7191  cnvinfex  7201  eqinfti  7203  infvalti  7205  ordiso2  7218  nninfninc  7306  nnnninfeq2  7312  isomni  7319  finomni  7323  exmidomni  7325  ctssexmid  7333  ismkv  7336  ismkvnex  7338  mkvprop  7341  fodjumkvlemres  7342  enmkvlem  7344  iswomni  7348  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  tapeq1  7454  exmidapne  7462  ccfunen  7466  ltsonq  7601  ltexnqq  7611  prcdnql  7687  prcunqu  7688  prloc  7694  prdisj  7695  genprndl  7724  genprndu  7725  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemcl  7879  caucvgprprlemcbv  7890  caucvgprprlemval  7891  suplocexprlemloc  7924  lttrsr  7965  ltsosr  7967  recexgt0sr  7976  mulgt0sr  7981  aptisr  7982  mulextsr1  7984  srpospr  7986  caucvgsrlemgt1  7998  caucvgsrlemoffres  8003  caucvgsr  8005  map2psrprg  8008  suplocsrlemb  8009  axprecex  8083  axpre-ltwlin  8086  axpre-lttrn  8087  axpre-apti  8088  axpre-mulgt0  8090  axpre-mulext  8091  axcaucvglemcau  8101  axcaucvglemres  8102  axpre-suploclemres  8104  axpre-suploc  8105  axsuploc  8235  ltleletr  8244  ltordlem  8645  squeeze0  9067  sup3exmid  9120  nnsub  9165  fzind  9578  uzind4s  9802  uzind4s2  9803  indstr  9805  supinfneg  9807  infsupneg  9808  frec2uzuzd  10641  frec2uzltd  10642  uzsinds  10683  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  monoord  10724  seq3split  10727  seqsplitg  10728  seqf1oglem2  10759  seqf1og  10760  seq3id2  10765  seqhomog  10769  expcl2lemap  10790  nn0ltexp2  10948  facdiv  10977  facwordi  10979  zfz1isolem1  11080  zfz1iso  11081  seq3coll  11082  wrdind  11275  wrd2ind  11276  swrdccatin1  11278  swrdccat3blem  11292  reuccatpfxs1lem  11299  caucvgre  11513  fimaxre2  11759  climcn1  11840  climcn2  11841  subcn2  11843  summodclem2a  11913  fsumsplitf  11940  fsum2d  11967  modfsummod  11990  fsumabs  11997  telfsumo  11998  fsumiun  12009  prodfdivap  12079  fprod2d  12155  fproddivapf  12163  fprodsplitf  12164  fprodsplit1f  12166  ndvdssub  12462  bezoutlemmain  12540  bezoutlemex  12543  bezoutlemzz  12544  bezoutlemsup  12551  dfgcd2  12556  algcvg  12591  algcvga  12594  algfx  12595  lcmgcdlem  12620  lcmdvds  12622  coprmgcdb  12631  coprmdvds1  12634  coprmdvds2  12636  prmind2  12663  dvdsprime  12665  nprm  12666  dvdsprm  12680  exprmfct  12681  isprm5lem  12684  coprm  12687  isprm6  12690  prmfac1  12695  sqrt2irr  12705  pcqmul  12847  pcqcl  12850  pc2dvds  12874  pcz  12876  prmpwdvds  12899  ennnfonelemim  13016  exmidunben  13018  infpn2  13048  setscomd  13094  mhmlem  13672  isnsg2  13761  ghmf1  13831  islring  14177  lringuplu  14181  rrgval  14247  rrgeq0i  14249  isdomn  14254  domneq0  14257  opprdomnbg  14259  znidom  14642  znrrg  14645  mplvalcoe  14675  mplsubgfilemcl  14684  uniopn  14696  fiinopn  14699  epttop  14785  cnpval  14893  iscnp  14894  icnpimaex  14906  lmcvg  14912  cnptoprest  14934  cnptoprest2  14935  lmss  14941  lmff  14944  txcnp  14966  txlm  14974  cnmpt12  14982  cnmpt22  14989  blssps  15122  blss  15123  metss  15189  comet  15194  metcnp3  15206  metcnp2  15208  txmetcnp  15213  divcnap  15260  mpomulcn  15261  elcncf2  15269  cncfi  15273  mulc1cncf  15284  cncfmet  15287  mulcncflem  15302  mulcncf  15303  dedekindeulemloc  15314  dedekindeulemlu  15316  dedekindeulemeu  15317  suplociccreex  15319  dedekindicclemloc  15323  dedekindicclemlu  15325  dedekindicclemeu  15326  ivthinclemlopn  15331  ivthinclemlr  15332  ivthinclemuopn  15333  ivthinclemur  15334  ivthinclemloc  15336  ivthreinc  15340  limccl  15354  ellimc3apf  15355  limccnpcntop  15370  limccnp2lem  15371  limccoap  15373  dvcoapbr  15402  dvmptfsum  15420  mpodvdsmulf1o  15685  perfectlem2  15695  lgsdir2lem4  15731  gausslemma2dlem0i  15757  lgseisenlem2  15771  lgsquad2lem2  15782  2sqlem6  15820  2sqlem8  15823  2sqlem10  15825  gropd  15869  grstructd2dom  15870  upgredg2vtx  15967  upgredgpr  15968  cbvrald  16261  bj-bdfindes  16421  bj-omtrans  16428  bj-inf2vnlem1  16442  bj-inf2vnlem2  16443  bj-inf2vnlem3  16444  bj-inf2vnlem4  16445  bj-findes  16453  strcoll2  16455  sscoll2  16460  subctctexmid  16479  pw1nct  16482  exmidsbthrlem  16504  sbthom  16508  apdiff  16530  ismkvnnlem  16534  nconstwlpolem  16547  neapmkv  16550  neap0mkv  16551  ltlenmkv  16552