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  840  nfbidf  1588  drnf1  1782  drnf2  1783  equveli  1808  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  mobidh  2114  mobid  2115  axext3  2215  cbvralfw  2766  cbvralf  2768  cbvralvw  2781  cbvraldva2  2784  gencbval  2862  vtoclgaf  2879  vtocl2gaf  2881  vtocl3gaf  2883  rspct  2913  rspc  2914  rspc2gv  2932  ceqex  2943  ralab2  2980  mob2  2996  mob  2998  morex  3000  reu7  3011  reu8  3012  nelrdva  3023  cdeqim  3034  sbcimg  3083  csbhypf  3176  cbvralcsf  3200  dfss2f  3228  sbcssg  3617  sneqrg  3865  elintab  3959  intss1  3963  intmin  3968  dfiin2g  4023  disji2  4100  disjiun  4103  trel  4214  trss  4216  bnd2  4285  zfpow  4287  exmidexmid  4308  exmidsssnc  4315  exmidundifim  4319  exmid1stab  4320  rext  4330  opth  4352  copsexg  4359  poeq1  4419  pocl  4423  swopolem  4425  swopo  4426  soeq1  4435  sowlin  4440  frforeq2  4465  frforeq3  4467  frirrg  4470  frind  4472  weeq1  4476  ordelord  4501  reusv3i  4579  ordtriexmid  4642  ontr2exmid  4646  onsucsssucexmid  4648  onsucelsucexmid  4651  ordsucunielexmid  4652  regexmidlem1  4654  regexmid  4656  reg2exmid  4657  elirr  4662  en2lp  4675  ordsoexmid  4683  onintexmid  4694  reg3exmid  4701  tfis  4704  tfisi  4708  peano2  4716  findes  4724  nnregexmid  4742  omsinds  4743  vtoclr  4797  poinxp  4818  soinxp  4819  posng  4821  ssrel  4837  ssrel2  4839  ssrelrel  4849  relop  4904  issref  5144  iotaexab  5330  iota5  5333  dffun4f  5367  sbcfung  5375  funopg  5385  brprcneu  5662  funfveu  5682  tz6.12f  5698  funbrfv  5712  ssimaexg  5738  fvmptss2  5751  fvmptssdm  5761  fvmptf  5769  fvelrn  5807  f1veqaeq  5941  dff13f  5942  isopolem  5994  isosolem  5996  riota5f  6029  imbrov2fvoveq  6074  oprabid  6081  ovmpos  6176  ov2gf  6177  ovi3  6190  caovcan  6218  caovordig  6219  caofrss  6297  caoftrn  6298  dfoprab4f  6386  f1o2ndf1  6423  poxp  6427  suppfnss  6456  smoel  6530  tfrlem1  6538  tfr1onlemsucfn  6570  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfr1onlemaccex  6578  tfr1onlemres  6579  tfrcllemsucfn  6583  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllembfn  6587  tfrcllemaccex  6591  tfrcllemres  6592  tfrcl  6594  nnsucelsuc  6723  nnsucsssuc  6724  nnmordi  6748  nnaordex  6760  qsel  6845  eroveu  6859  ecopovtrn  6865  ecopovtrng  6868  th3qlem2  6871  ixpsnf1o  6970  fundmeng  7047  modom  7060  phplem3g  7109  nneneq  7110  ssfiexmid  7130  ssfiexmidt  7132  domfiexmid  7134  findcard  7144  findcard2  7145  findcard2s  7146  findcard2d  7147  findcard2sd  7148  diffifi  7150  ac6sfi  7154  fiintim  7190  fisseneq  7194  fidcenumlemrk  7223  fidcenumlemr  7224  isbth  7236  supeq3  7280  supeq123d  7281  supmoti  7283  suplubti  7290  supisolem  7298  cnvinfex  7308  eqinfti  7310  infvalti  7312  ordiso2  7325  nninfninc  7413  nnnninfeq2  7419  isomni  7426  finomni  7430  exmidomni  7432  ctssexmid  7440  ismkv  7443  ismkvnex  7445  mkvprop  7448  fodjumkvlemres  7449  enmkvlem  7451  iswomni  7455  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  papsym  7560  papcotr  7561  tapeq1  7565  exmidapne  7573  ccfunen  7577  ltsonq  7712  ltexnqq  7722  prcdnql  7798  prcunqu  7799  prloc  7805  prdisj  7806  genprndl  7835  genprndu  7836  caucvgprlemnkj  7980  caucvgprlemnbj  7981  caucvgprlemcl  7990  caucvgprprlemcbv  8001  caucvgprprlemval  8002  suplocexprlemloc  8035  lttrsr  8076  ltsosr  8078  recexgt0sr  8087  mulgt0sr  8092  aptisr  8093  mulextsr1  8095  srpospr  8097  caucvgsrlemgt1  8109  caucvgsrlemoffres  8114  caucvgsr  8116  map2psrprg  8119  suplocsrlemb  8120  axprecex  8194  axpre-ltwlin  8197  axpre-lttrn  8198  axpre-apti  8199  axpre-mulgt0  8201  axpre-mulext  8202  axcaucvglemcau  8212  axcaucvglemres  8213  axpre-suploclemres  8215  axpre-suploc  8216  axsuploc  8345  ltleletr  8354  ltordlem  8755  squeeze0  9177  sup3exmid  9230  nnsub  9275  fzind  9692  uzind4s  9921  uzind4s2  9922  indstr  9924  supinfneg  9926  infsupneg  9927  frec2uzuzd  10763  frec2uzltd  10764  uzsinds  10805  seq3fveq2  10836  seqfveq2g  10838  seq3shft2  10842  seqshft2g  10843  monoord  10846  seq3split  10849  seqsplitg  10850  seqf1oglem2  10881  seqf1og  10882  seq3id2  10887  seqhomog  10891  expcl2lemap  10912  nn0ltexp2  11070  facdiv  11099  facwordi  11101  zfz1isolem1  11208  zfz1iso  11209  seq3coll  11210  wrdind  11410  wrd2ind  11411  swrdccatin1  11413  swrdccat3blem  11427  reuccatpfxs1lem  11434  caucvgre  11662  fimaxre2  11908  climcn1  11989  climcn2  11990  subcn2  11992  summodclem2a  12063  fsumsplitf  12090  fsum2d  12117  modfsummod  12140  fsumabs  12147  telfsumo  12148  fsumiun  12159  prodfdivap  12229  fprod2d  12305  fproddivapf  12313  fprodsplitf  12314  fprodsplit1f  12316  ndvdssub  12612  bezoutlemmain  12690  bezoutlemex  12693  bezoutlemzz  12694  bezoutlemsup  12701  dfgcd2  12706  algcvg  12741  algcvga  12744  algfx  12745  lcmgcdlem  12770  lcmdvds  12772  coprmgcdb  12781  coprmdvds1  12784  coprmdvds2  12786  prmind2  12813  dvdsprime  12815  nprm  12816  dvdsprm  12830  exprmfct  12831  isprm5lem  12834  coprm  12837  isprm6  12840  prmfac1  12845  sqrt2irr  12855  pcqmul  12997  pcqcl  13000  pc2dvds  13024  pcz  13026  prmpwdvds  13049  ennnfonelemim  13167  exmidunben  13169  infpn2  13199  setscomd  13245  mhmlem  13823  isnsg2  13912  ghmf1  13982  islring  14329  lringuplu  14333  rrgval  14399  rrgeq0i  14401  isdomn  14407  domneq0  14410  opprdomnbg  14412  znidom  14797  znrrg  14800  mplvalcoe  14837  mplsubgfilemcl  14846  uniopn  14858  fiinopn  14861  epttop  14947  cnpval  15055  iscnp  15056  icnpimaex  15068  lmcvg  15074  cnptoprest  15096  cnptoprest2  15097  lmss  15103  lmff  15106  txcnp  15128  txlm  15136  cnmpt12  15144  cnmpt22  15151  blssps  15284  blss  15285  metss  15351  comet  15356  metcnp3  15368  metcnp2  15370  txmetcnp  15375  divcnap  15422  mpomulcn  15423  elcncf2  15431  cncfi  15435  mulc1cncf  15446  cncfmet  15449  mulcncflem  15464  mulcncf  15465  dedekindeulemloc  15476  dedekindeulemlu  15478  dedekindeulemeu  15479  suplociccreex  15481  dedekindicclemloc  15485  dedekindicclemlu  15487  dedekindicclemeu  15488  ivthinclemlopn  15493  ivthinclemlr  15494  ivthinclemuopn  15495  ivthinclemur  15496  ivthinclemloc  15498  ivthreinc  15502  limccl  15516  ellimc3apf  15517  limccnpcntop  15532  limccnp2lem  15533  limccoap  15535  dvcoapbr  15564  dvmptfsum  15582  mpodvdsmulf1o  15850  perfectlem2  15860  lgsdir2lem4  15896  gausslemma2dlem0i  15922  lgseisenlem2  15936  lgsquad2lem2  15947  2sqlem6  15985  2sqlem8  15988  2sqlem10  15990  gropd  16034  grstructd2dom  16035  upgredg2vtx  16135  upgredgpr  16136  eupth2fi  16466  cbvrald  16552  bj-bdfindes  16711  bj-omtrans  16718  bj-inf2vnlem1  16732  bj-inf2vnlem2  16733  bj-inf2vnlem3  16734  bj-inf2vnlem4  16735  bj-findes  16743  strcoll2  16745  sscoll2  16750  subctctexmid  16766  pw1nct  16769  exmidnotnotr  16771  exmidcon  16772  exmidsbthrlem  16794  sbthom  16798  apdiff  16824  ismkvnnlem  16829  nconstwlpolem  16842  neapmkv  16845  neap0mkv  16846  ltlenmkv  16847