ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi12d GIF version

Theorem anbi12d 457
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
anbi12d.1 (𝜑 → (𝜓𝜒))
anbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
anbi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem anbi12d
StepHypRef Expression
1 anbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21anbi1d 453 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 anbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43anbi2d 452 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 186 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.38  570  pm5.17dc  846  orbididc  897  3anbi123d  1246  xorbi2d  1314  xorbi1d  1315  drsb1  1724  mopick  2023  clelab  2209  cbvrexf  2581  cbvreu  2584  cbvrexdva2  2591  cbvrab  2613  gencbvex  2659  rspce  2710  eqvincf  2733  ceqsrexv  2738  elrabf  2760  rexab2  2772  reu2  2794  reu6  2795  rmo4  2799  reu8  2802  reuind  2809  sbcan  2870  sbcang  2871  sbcabel  2909  rmob  2920  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  difjust  2989  injust  2993  eldif  2997  ssconb  3122  elin  3172  opeq1  3605  opeq2  3606  2ralunsn  3625  elunii  3641  csbunig  3644  eluniab  3648  cbvopab  3884  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  cbvopab2v  3890  cbvmptf  3907  cbvmpt  3908  trel  3918  nalset  3944  elssabg  3959  mss  4027  exss  4028  opelopab2a  4066  poeq1  4100  pocl  4104  soeq1  4116  weeq1  4157  weeq2  4158  ordeq  4173  zfun  4235  snnex  4245  reusv3  4256  ontr2exmid  4314  regexmid  4324  onintexmid  4361  reg3exmid  4368  peano5  4386  limom  4401  nnregexmid  4407  vtoclr  4454  opeliunxp  4461  poinxp  4475  opbrop  4485  csbxpg  4487  opeliunxp2  4544  relop  4554  brcogw  4573  elrnmpt1  4654  elsnres  4716  dfres2  4731  inimasn  4815  xpcanm  4836  xpcan2m  4837  elxp4  4884  elxp5  4885  cnvsom  4940  sbcfung  5004  funopg  5013  fununi  5047  funcnvuni  5048  fneq1  5067  2elresin  5090  feq1  5110  sbcfng  5124  sbcfg  5125  f1eq1  5174  foeq1  5192  f1oeq1  5207  f1oeq2  5208  f1oeq3  5209  ffoss  5248  brprcneu  5261  fv3  5291  tz6.12f  5296  ssimaex  5328  fvopab3g  5340  fvopab3ig  5341  fvopab6  5359  fmptco  5427  elunirn  5506  f1imaeq  5515  foeqcnvco  5530  fliftfun  5536  fliftval  5540  isoeq1  5541  isoeq4  5544  isoini  5558  isopolem  5562  f1oiso2  5567  riotabidv  5571  cbvriota  5579  acexmid  5612  cbvoprab1  5677  cbvoprab2  5678  cbvoprab12  5679  cbvmpt2x  5683  ov  5721  ovig  5723  ovg  5740  caovimo  5795  caoftrn  5837  opabex3d  5849  opabex3  5850  elxp6  5897  unielxp  5901  dfoprab4  5919  dfoprab4f  5920  fmpt2x  5927  xporderlem  5953  poxp  5954  cnvoprab  5956  f1od2  5957  sprmpt2  5961  isprmpt2  5962  dftpos4  5982  tpostpos  5983  smoiso  6021  tfrlem3ag  6028  tfrlem3a  6029  tfr0dm  6041  tfrlemisucaccv  6044  tfrlemiex  6050  tfrlemi1  6051  tfrlemi14d  6052  tfrexlem  6053  tfr1onlem3ag  6056  tfr1onlemsucaccv  6060  tfr1onlemex  6066  tfr1onlemaccex  6067  tfr1onlemres  6068  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllemex  6079  tfrcllemaccex  6080  tfrcllemres  6081  tfrcldm  6082  frec0g  6116  frecabcl  6118  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  nnacan  6223  nnmcan  6230  nnaordex  6238  ertr  6259  brecop  6334  eroveu  6335  ecopovtrn  6341  ecopovtrng  6344  th3qlem1  6346  th3qlem2  6347  th3q  6349  elpm2r  6375  mapsncnv  6404  mapsnen  6480  map1  6481  xpsnen  6489  endisj  6492  xpf1o  6512  phplem3g  6524  ssfiexmid  6544  domfiexmid  6546  findcard2s  6558  isinfinf  6565  ac6sfi  6566  fisseneq  6592  f1dmvrnfibi  6603  sbthlem2  6611  isbth  6620  supeq1  6625  supeq3  6629  supeq123d  6630  supmoti  6632  eqsupti  6635  supsnti  6644  isotilem  6645  isoti  6646  supisolem  6647  supisoex  6648  cnvinfex  6657  cnvti  6658  eqinfti  6659  infvalti  6661  updjud  6717  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  ltsopi  6823  recexnq  6893  recmulnqg  6894  ltsonq  6901  lt2addnq  6907  lt2mulnq  6908  ltbtwnnqq  6918  prarloclemarch2  6922  enq0sym  6935  enq0ref  6936  enq0tr  6937  enq0breq  6939  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  mulnnnq0  6953  nqnq0a  6957  nqnq0m  6958  elinp  6977  prcdnql  6987  prcunqu  6988  prltlu  6990  prdisj  6995  prarloclemlo  6997  prarloclem3  7000  prarloclem5  7003  ltdfpr  7009  genprndl  7024  genprndu  7025  genpdisj  7026  appdivnq  7066  ltpopr  7098  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  ltexpri  7116  recexprlemm  7127  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  recexpr  7141  aptiprleml  7142  archpr  7146  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlemlim  7164  cauappcvgpr  7165  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemcl  7179  caucvgpr  7185  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemopu  7202  caucvgprpr  7215  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  lttrsr  7252  recexgt0sr  7263  caucvgsrlemcau  7282  caucvgsrlemgt1  7284  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  caucvgsr  7291  ltresr  7320  pitonn  7329  peano1nnnn  7333  peano2nnnn  7334  axprecex  7359  axcnre  7360  axpre-lttrn  7363  peano5nnnn  7371  axcaucvglemcau  7377  axcaucvglemres  7378  axlttrn  7499  letri3  7510  letr  7512  le2add  7866  lt2add  7867  ltleadd  7868  lt2sub  7882  le2sub  7883  apreap  8005  apreim  8021  apti  8040  msq11  8298  dfinfre  8352  cju  8356  peano5nni  8360  1nn  8368  peano2nn  8369  nn2ge  8389  nominpos  8586  elz2  8751  dfuzi  8789  uzind  8790  supinfneg  9015  infsupneg  9016  xrletri3  9202  xrletr  9205  z2ge  9220  elixx1  9247  elioo2  9271  iooshf  9302  iooneg  9337  iccneg  9338  icoshft  9339  elfz1  9361  fzdifsuc  9425  fzrev  9428  1fv  9478  exbtwnzlemstep  9587  exbtwnzlemshrink  9588  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2zlemshrink  9593  rebtwn2z  9594  qbtwnre  9596  qbtwnxr  9597  flval  9607  flqlelt  9611  flqbi  9625  flqbi2  9626  modqid2  9686  q2submod  9720  nnesq  9969  hashunlem  10108  zfz1isolem1  10141  zfz1iso  10142  iseqcoll  10143  shftlem  10146  shftfibg  10150  shftfib  10153  shftfn  10154  2shfti  10161  cjval  10174  cjth  10175  remim  10189  caucvgrelemcau  10308  caucvgre  10309  cvg1nlemcau  10312  cvg1nlemres  10313  rexanuz2  10319  recvguniq  10323  resqrexlemgt0  10348  resqrexlemoverl  10349  resqrexlemglsq  10350  resqrexlemsqa  10352  resqrexlemex  10353  rsqrmo  10355  resqrtcl  10357  rersqrtthlem  10358  absdiflt  10420  absdifle  10421  cau3lem  10442  icodiamlt  10508  maxleast  10541  negfi  10552  minmax  10554  lemininf  10557  ltmininf  10558  clim  10562  clim2  10564  climshftlemg  10583  addcn2  10591  climcau  10626  isummo  10662  fisum  10665  divalgmod  10802  ndvdssub  10805  zsupcllemstep  10816  infssuzex  10820  gcdsupex  10824  gcdsupcl  10825  gcddvds  10830  dvdslegcd  10831  bezoutlemmain  10862  bezoutlemex  10865  bezoutlemzz  10866  bezoutlemeu  10871  bezoutlemle  10872  bezoutlemsup  10873  dfgcd3  10874  dfgcd2  10878  gcddiv  10883  lcmval  10920  lcmcllem  10924  dvdslcm  10926  lcmledvds  10927  lcmgcdlem  10934  lcmdvds  10936  coprmgcdb  10945  ncoprmgcdne1b  10946  coprmdvds1  10948  qredeu  10954  divgcdcoprm0  10958  divgcdcoprmex  10959  isprm3  10975  pw2dvdslemn  11018  pw2dvdseu  11021  oddpwdclemxy  11022  qnumdencl  11040  qnumdenbi  11045  crth  11075  bj-sseq  11130  bj-nalset  11224  bj-indeq  11262  bj-2inf  11271  exmidsbthrlem  11350  qdencn  11353
  Copyright terms: Public domain W3C validator