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  1781  drnf2  1782  equveli  1807  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  mobidh  2113  mobid  2114  axext3  2214  cbvralfw  2757  cbvralf  2759  cbvralvw  2772  cbvraldva2  2775  gencbval  2853  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  rspct  2904  rspc  2905  rspc2gv  2923  ceqex  2934  ralab2  2971  mob2  2987  mob  2989  morex  2991  reu7  3002  reu8  3003  nelrdva  3014  cdeqim  3025  sbcimg  3074  csbhypf  3167  cbvralcsf  3191  dfss2f  3219  sbcssg  3605  sneqrg  3850  elintab  3944  intss1  3948  intmin  3953  dfiin2g  4008  disji2  4085  disjiun  4088  trel  4199  trss  4201  bnd2  4269  zfpow  4271  exmidexmid  4292  exmidsssnc  4299  exmidundifim  4303  exmid1stab  4304  rext  4313  opth  4335  copsexg  4342  poeq1  4402  pocl  4406  swopolem  4408  swopo  4409  soeq1  4418  sowlin  4423  frforeq2  4448  frforeq3  4450  frirrg  4453  frind  4455  weeq1  4459  ordelord  4484  reusv3i  4562  ordtriexmid  4625  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  ordsucunielexmid  4635  regexmidlem1  4637  regexmid  4639  reg2exmid  4640  elirr  4645  en2lp  4658  ordsoexmid  4666  onintexmid  4677  reg3exmid  4684  tfis  4687  tfisi  4691  peano2  4699  findes  4707  nnregexmid  4725  omsinds  4726  vtoclr  4780  poinxp  4801  soinxp  4802  posng  4804  ssrel  4820  ssrel2  4822  ssrelrel  4832  relop  4886  issref  5126  iotaexab  5312  iota5  5315  dffun4f  5349  sbcfung  5357  funopg  5367  brprcneu  5641  funfveu  5661  tz6.12f  5677  funbrfv  5691  ssimaexg  5717  fvmptss2  5730  fvmptssdm  5740  fvmptf  5748  fvelrn  5786  f1veqaeq  5920  dff13f  5921  isopolem  5973  isosolem  5975  riota5f  6008  imbrov2fvoveq  6053  oprabid  6060  ovmpos  6155  ov2gf  6156  ovi3  6169  caovcan  6197  caovordig  6198  caofrss  6276  caoftrn  6277  dfoprab4f  6365  f1o2ndf1  6402  poxp  6406  suppfnss  6435  smoel  6509  tfrlem1  6517  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  nnsucelsuc  6702  nnsucsssuc  6703  nnmordi  6727  nnaordex  6739  qsel  6824  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem2  6850  ixpsnf1o  6948  fundmeng  7025  modom  7037  phplem3g  7085  nneneq  7086  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard  7120  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  diffifi  7126  ac6sfi  7130  fiintim  7166  fisseneq  7170  fidcenumlemrk  7196  fidcenumlemr  7197  isbth  7209  supeq3  7232  supeq123d  7233  supmoti  7235  suplubti  7242  supisolem  7250  cnvinfex  7260  eqinfti  7262  infvalti  7264  ordiso2  7277  nninfninc  7365  nnnninfeq2  7371  isomni  7378  finomni  7382  exmidomni  7384  ctssexmid  7392  ismkv  7395  ismkvnex  7397  mkvprop  7400  fodjumkvlemres  7401  enmkvlem  7403  iswomni  7407  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  tapeq1  7514  exmidapne  7522  ccfunen  7526  ltsonq  7661  ltexnqq  7671  prcdnql  7747  prcunqu  7748  prloc  7754  prdisj  7755  genprndl  7784  genprndu  7785  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemcl  7939  caucvgprprlemcbv  7950  caucvgprprlemval  7951  suplocexprlemloc  7984  lttrsr  8025  ltsosr  8027  recexgt0sr  8036  mulgt0sr  8041  aptisr  8042  mulextsr1  8044  srpospr  8046  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  caucvgsr  8065  map2psrprg  8068  suplocsrlemb  8069  axprecex  8143  axpre-ltwlin  8146  axpre-lttrn  8147  axpre-apti  8148  axpre-mulgt0  8150  axpre-mulext  8151  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  axsuploc  8295  ltleletr  8304  ltordlem  8705  squeeze0  9127  sup3exmid  9180  nnsub  9225  fzind  9638  uzind4s  9867  uzind4s2  9868  indstr  9870  supinfneg  9872  infsupneg  9873  frec2uzuzd  10708  frec2uzltd  10709  uzsinds  10750  seq3fveq2  10781  seqfveq2g  10783  seq3shft2  10787  seqshft2g  10788  monoord  10791  seq3split  10794  seqsplitg  10795  seqf1oglem2  10826  seqf1og  10827  seq3id2  10832  seqhomog  10836  expcl2lemap  10857  nn0ltexp2  11015  facdiv  11044  facwordi  11046  zfz1isolem1  11148  zfz1iso  11149  seq3coll  11150  wrdind  11350  wrd2ind  11351  swrdccatin1  11353  swrdccat3blem  11367  reuccatpfxs1lem  11374  caucvgre  11602  fimaxre2  11848  climcn1  11929  climcn2  11930  subcn2  11932  summodclem2a  12003  fsumsplitf  12030  fsum2d  12057  modfsummod  12080  fsumabs  12087  telfsumo  12088  fsumiun  12099  prodfdivap  12169  fprod2d  12245  fproddivapf  12253  fprodsplitf  12254  fprodsplit1f  12256  ndvdssub  12552  bezoutlemmain  12630  bezoutlemex  12633  bezoutlemzz  12634  bezoutlemsup  12641  dfgcd2  12646  algcvg  12681  algcvga  12684  algfx  12685  lcmgcdlem  12710  lcmdvds  12712  coprmgcdb  12721  coprmdvds1  12724  coprmdvds2  12726  prmind2  12753  dvdsprime  12755  nprm  12756  dvdsprm  12770  exprmfct  12771  isprm5lem  12774  coprm  12777  isprm6  12780  prmfac1  12785  sqrt2irr  12795  pcqmul  12937  pcqcl  12940  pc2dvds  12964  pcz  12966  prmpwdvds  12989  ennnfonelemim  13106  exmidunben  13108  infpn2  13138  setscomd  13184  mhmlem  13762  isnsg2  13851  ghmf1  13921  islring  14268  lringuplu  14272  rrgval  14338  rrgeq0i  14340  isdomn  14345  domneq0  14348  opprdomnbg  14350  znidom  14733  znrrg  14736  mplvalcoe  14771  mplsubgfilemcl  14780  uniopn  14792  fiinopn  14795  epttop  14881  cnpval  14989  iscnp  14990  icnpimaex  15002  lmcvg  15008  cnptoprest  15030  cnptoprest2  15031  lmss  15037  lmff  15040  txcnp  15062  txlm  15070  cnmpt12  15078  cnmpt22  15085  blssps  15218  blss  15219  metss  15285  comet  15290  metcnp3  15302  metcnp2  15304  txmetcnp  15309  divcnap  15356  mpomulcn  15357  elcncf2  15365  cncfi  15369  mulc1cncf  15380  cncfmet  15383  mulcncflem  15398  mulcncf  15399  dedekindeulemloc  15410  dedekindeulemlu  15412  dedekindeulemeu  15413  suplociccreex  15415  dedekindicclemloc  15419  dedekindicclemlu  15421  dedekindicclemeu  15422  ivthinclemlopn  15427  ivthinclemlr  15428  ivthinclemuopn  15429  ivthinclemur  15430  ivthinclemloc  15432  ivthreinc  15436  limccl  15450  ellimc3apf  15451  limccnpcntop  15466  limccnp2lem  15467  limccoap  15469  dvcoapbr  15498  dvmptfsum  15516  mpodvdsmulf1o  15784  perfectlem2  15794  lgsdir2lem4  15830  gausslemma2dlem0i  15856  lgseisenlem2  15870  lgsquad2lem2  15881  2sqlem6  15919  2sqlem8  15922  2sqlem10  15924  gropd  15968  grstructd2dom  15969  upgredg2vtx  16069  upgredgpr  16070  eupth2fi  16400  cbvrald  16486  bj-bdfindes  16645  bj-omtrans  16652  bj-inf2vnlem1  16666  bj-inf2vnlem2  16667  bj-inf2vnlem3  16668  bj-inf2vnlem4  16669  bj-findes  16677  strcoll2  16679  sscoll2  16684  subctctexmid  16702  pw1nct  16705  exmidnotnotr  16707  exmidcon  16708  exmidsbthrlem  16730  sbthom  16734  apdiff  16760  ismkvnnlem  16765  nconstwlpolem  16778  neapmkv  16781  neap0mkv  16782  ltlenmkv  16783