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  822  nfbidf  1527  drnf1  1721  drnf2  1722  equveli  1747  ax11v2  1808  ax11v  1815  ax11ev  1816  equs5or  1818  mobidh  2048  mobid  2049  axext3  2148  cbvralfw  2682  cbvralf  2684  cbvralvw  2695  cbvraldva2  2698  gencbval  2773  vtoclgaf  2790  vtocl2gaf  2792  vtocl3gaf  2794  rspct  2822  rspc  2823  rspc2gv  2841  ceqex  2852  ralab2  2889  mob2  2905  mob  2907  morex  2909  reu7  2920  reu8  2921  nelrdva  2932  cdeqim  2943  sbcimg  2991  csbhypf  3082  cbvralcsf  3106  dfss2f  3132  sbcssg  3517  sneqrg  3741  elintab  3834  intss1  3838  intmin  3843  dfiin2g  3898  disji2  3974  disjiun  3976  trel  4086  trss  4088  bnd2  4151  zfpow  4153  exmidexmid  4174  exmidsssnc  4181  exmidundifim  4185  rext  4192  opth  4214  copsexg  4221  poeq1  4276  pocl  4280  swopolem  4282  swopo  4283  soeq1  4292  sowlin  4297  frforeq2  4322  frforeq3  4324  frirrg  4327  frind  4329  weeq1  4333  ordelord  4358  reusv3i  4436  ordtriexmid  4497  ontr2exmid  4501  onsucsssucexmid  4503  onsucelsucexmid  4506  ordsucunielexmid  4507  regexmidlem1  4509  regexmid  4511  reg2exmid  4512  elirr  4517  en2lp  4530  ordsoexmid  4538  onintexmid  4549  reg3exmid  4556  tfis  4559  tfisi  4563  peano2  4571  findes  4579  nnregexmid  4597  omsinds  4598  vtoclr  4651  poinxp  4672  soinxp  4673  posng  4675  ssrel  4691  ssrel2  4693  ssrelrel  4703  relop  4753  issref  4985  iota5  5172  dffun4f  5203  sbcfung  5211  funopg  5221  brprcneu  5478  funfveu  5498  tz6.12f  5514  funbrfv  5524  ssimaexg  5547  fvmptss2  5560  fvmptssdm  5569  fvmptf  5577  fvelrn  5615  f1veqaeq  5736  dff13f  5737  isopolem  5789  isosolem  5791  riota5f  5821  imbrov2fvoveq  5866  oprabid  5870  ovmpos  5961  ov2gf  5962  ovi3  5974  caovcan  6002  caovordig  6003  caofrss  6073  caoftrn  6074  dfoprab4f  6158  f1o2ndf1  6192  poxp  6196  smoel  6264  tfrlem1  6272  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemaccex  6325  tfrcllemres  6326  tfrcl  6328  nnsucelsuc  6455  nnsucsssuc  6456  nnmordi  6480  nnaordex  6491  qsel  6574  eroveu  6588  ecopovtrn  6594  ecopovtrng  6597  th3qlem2  6600  ixpsnf1o  6698  fundmeng  6769  phplem3g  6818  nneneq  6819  ssfiexmid  6838  domfiexmid  6840  findcard  6850  findcard2  6851  findcard2s  6852  findcard2d  6853  findcard2sd  6854  diffifi  6856  ac6sfi  6860  fiintim  6890  fisseneq  6893  fidcenumlemrk  6915  fidcenumlemr  6916  isbth  6928  supeq3  6951  supeq123d  6952  supmoti  6954  suplubti  6961  supisolem  6969  cnvinfex  6979  eqinfti  6981  infvalti  6983  ordiso2  6996  nnnninfeq2  7089  isomni  7096  finomni  7100  exmidomni  7102  ctssexmid  7110  ismkv  7113  ismkvnex  7115  mkvprop  7118  fodjumkvlemres  7119  enmkvlem  7121  iswomni  7125  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  ccfunen  7201  ltsonq  7335  ltexnqq  7345  prcdnql  7421  prcunqu  7422  prloc  7428  prdisj  7429  genprndl  7458  genprndu  7459  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemcl  7613  caucvgprprlemcbv  7624  caucvgprprlemval  7625  suplocexprlemloc  7658  lttrsr  7699  ltsosr  7701  recexgt0sr  7710  mulgt0sr  7715  aptisr  7716  mulextsr1  7718  srpospr  7720  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  caucvgsr  7739  map2psrprg  7742  suplocsrlemb  7743  axprecex  7817  axpre-ltwlin  7820  axpre-lttrn  7821  axpre-apti  7822  axpre-mulgt0  7824  axpre-mulext  7825  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  axpre-suploc  7839  axsuploc  7967  ltleletr  7976  ltordlem  8376  squeeze0  8795  sup3exmid  8848  nnsub  8892  fzind  9302  uzind4s  9524  uzind4s2  9525  indstr  9527  supinfneg  9529  infsupneg  9530  frec2uzuzd  10333  frec2uzltd  10334  uzsinds  10373  seq3fveq2  10400  seq3shft2  10404  monoord  10407  seq3split  10410  seq3id2  10440  expcl2lemap  10463  nn0ltexp2  10619  facdiv  10647  facwordi  10649  zfz1isolem1  10749  zfz1iso  10750  seq3coll  10751  caucvgre  10919  fimaxre2  11164  climcn1  11245  climcn2  11246  subcn2  11248  summodclem2a  11318  fsumsplitf  11345  fsum2d  11372  modfsummod  11395  fsumabs  11402  telfsumo  11403  fsumiun  11414  prodfdivap  11484  fprod2d  11560  fproddivapf  11568  fprodsplitf  11569  fprodsplit1f  11571  ndvdssub  11863  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemzz  11931  bezoutlemsup  11938  dfgcd2  11943  algcvg  11976  algcvga  11979  algfx  11980  lcmgcdlem  12005  lcmdvds  12007  coprmgcdb  12016  coprmdvds1  12019  coprmdvds2  12021  prmind2  12048  dvdsprime  12050  nprm  12051  dvdsprm  12065  exprmfct  12066  isprm5lem  12069  coprm  12072  isprm6  12075  prmfac1  12080  sqrt2irr  12090  pcqmul  12231  pcqcl  12234  pc2dvds  12257  pcz  12259  prmpwdvds  12281  ennnfonelemim  12353  exmidunben  12355  infpn2  12385  uniopn  12599  fiinopn  12602  epttop  12690  cnpval  12798  iscnp  12799  icnpimaex  12811  lmcvg  12817  cnptoprest  12839  cnptoprest2  12840  lmss  12846  lmff  12849  txcnp  12871  txlm  12879  cnmpt12  12887  cnmpt22  12894  blssps  13027  blss  13028  metss  13094  comet  13099  metcnp3  13111  metcnp2  13113  txmetcnp  13118  divcnap  13155  elcncf2  13161  cncfi  13165  mulc1cncf  13176  cncfmet  13179  mulcncflem  13190  mulcncf  13191  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeulemeu  13200  suplociccreex  13202  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemeu  13209  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  limccl  13228  ellimc3apf  13229  limccnpcntop  13244  limccnp2lem  13245  limccoap  13247  dvcoapbr  13271  lgsdir2lem4  13532  2sqlem6  13556  2sqlem8  13559  2sqlem10  13561  cbvrald  13629  bj-bdfindes  13791  bj-omtrans  13798  bj-inf2vnlem1  13812  bj-inf2vnlem2  13813  bj-inf2vnlem3  13814  bj-inf2vnlem4  13815  bj-findes  13823  strcoll2  13825  sscoll2  13830  exmid1stab  13840  subctctexmid  13841  pw1nct  13843  exmidsbthrlem  13861  sbthom  13865  apdiff  13887  ismkvnnlem  13891  nconstwlpolem  13903  neapmkv  13906