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

Theorem anbi12d 464
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
anbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
anbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
anbi12d  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )

Proof of Theorem anbi12d
StepHypRef Expression
1 anbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21anbi1d 460 . 2  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
3 anbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43anbi2d 459 . 2  |-  ( ph  ->  ( ( ch  /\  th )  <->  ( ch  /\  ta ) ) )
52, 4bitrd 187 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> 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:  pm4.38  579  pm5.17dc  874  orbididc  922  3anbi123d  1275  xorbi2d  1343  xorbi1d  1344  drsb1  1755  mopick  2055  clelab  2242  cbvrexf  2626  cbvreu  2629  cbvrexdva2  2636  cbvrab  2658  gencbvex  2706  rspce  2758  eqvincf  2784  ceqsrexv  2789  elrabf  2811  rexab2  2823  reu2  2845  reu6  2846  rmo4  2850  reu8  2853  reuind  2862  sbcan  2923  sbcang  2924  sbcabel  2962  rmob  2973  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  difjust  3042  injust  3046  eldif  3050  ssconb  3179  elin  3229  opeq1  3675  opeq2  3676  2ralunsn  3695  elunii  3711  csbunig  3714  eluniab  3718  cbvopab  3969  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  cbvopab2v  3975  cbvmptf  3992  cbvmpt  3993  trel  4003  nalset  4028  elssabg  4043  mss  4118  exss  4119  opelopab2a  4157  poeq1  4191  pocl  4195  soeq1  4207  weeq1  4248  weeq2  4249  ordeq  4264  zfun  4326  snnex  4339  reusv3  4351  ontr2exmid  4410  regexmid  4420  onintexmid  4457  reg3exmid  4464  peano5  4482  limom  4497  nnregexmid  4504  vtoclr  4557  opeliunxp  4564  poinxp  4578  opbrop  4588  csbxpg  4590  opeliunxp2  4649  relop  4659  brcogw  4678  elrnmpt1  4760  elsnres  4826  dfres2  4841  inimasn  4926  xpcanm  4948  xpcan2m  4949  elxp4  4996  elxp5  4997  cnvsom  5052  sbcfung  5117  funopg  5127  fununi  5161  funcnvuni  5162  fneq1  5181  2elresin  5204  feq1  5225  sbcfng  5240  sbcfg  5241  f1eq1  5293  foeq1  5311  f1oeq1  5326  f1oeq2  5327  f1oeq3  5328  ffoss  5367  brprcneu  5382  fv3  5412  tz6.12f  5418  ssimaex  5450  fvopab3g  5462  fvopab3ig  5463  fvopab6  5485  fmptco  5554  elunirn  5635  f1imaeq  5644  foeqcnvco  5659  fliftfun  5665  fliftval  5669  isoeq1  5670  isoeq4  5673  isoini  5687  isopolem  5691  f1oiso2  5696  riotabidv  5700  cbvriota  5708  acexmid  5741  ovanraleqv  5766  cbvoprab1  5811  cbvoprab2  5812  cbvoprab12  5813  cbvmpox  5817  ov  5858  ovig  5860  ovg  5877  caovimo  5932  caoftrn  5975  opabex3d  5987  opabex3  5988  elxp6  6035  unielxp  6040  dfoprab4  6058  dfoprab4f  6059  fmpox  6066  xporderlem  6096  poxp  6097  cnvoprab  6099  f1od2  6100  opeliunxp2f  6103  rbropapd  6107  dftpos4  6128  tpostpos  6129  smoiso  6167  tfrlem3ag  6174  tfrlem3a  6175  tfr0dm  6187  tfrlemisucaccv  6190  tfrlemiex  6196  tfrlemi1  6197  tfrlemi14d  6198  tfrexlem  6199  tfr1onlem3ag  6202  tfr1onlemsucaccv  6206  tfr1onlemex  6212  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllemex  6225  tfrcllemaccex  6226  tfrcllemres  6227  tfrcldm  6228  frec0g  6262  frecabcl  6264  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  nnacan  6376  nnmcan  6383  nnaordex  6391  ertr  6412  brecop  6487  eroveu  6488  ecopovtrn  6494  ecopovtrng  6497  th3qlem1  6499  th3qlem2  6500  th3q  6502  elpm2r  6528  mapsncnv  6557  elixp2  6564  ixpeq1  6571  elixpsn  6597  ixpsnf1o  6598  mapsnen  6673  map1  6674  xpsnen  6683  endisj  6686  xpf1o  6706  phplem3g  6718  ssfiexmid  6738  domfiexmid  6740  findcard2s  6752  isinfinf  6759  ac6sfi  6760  fiintim  6785  fisseneq  6788  f1dmvrnfibi  6800  sbthlem2  6814  isbth  6823  supeq1  6841  supeq3  6845  supeq123d  6846  supmoti  6848  eqsupti  6851  supsnti  6860  isotilem  6861  isoti  6862  supisolem  6863  supisoex  6864  cnvinfex  6873  cnvti  6874  eqinfti  6875  infvalti  6877  updjud  6935  ctssexmid  6992  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  acfun  7031  ccfunen  7047  ltsopi  7096  recexnq  7166  recmulnqg  7167  ltsonq  7174  lt2addnq  7180  lt2mulnq  7181  ltbtwnnqq  7191  prarloclemarch2  7195  enq0sym  7208  enq0ref  7209  enq0tr  7210  enq0breq  7212  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  mulnnnq0  7226  nqnq0a  7230  nqnq0m  7231  elinp  7250  prcdnql  7260  prcunqu  7261  prltlu  7263  prdisj  7268  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  ltdfpr  7282  genprndl  7297  genprndu  7298  genpdisj  7299  appdivnq  7339  ltpopr  7371  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  ltexpri  7389  recexprlemm  7400  recexprlemdisj  7406  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  recexpr  7414  aptiprleml  7415  archpr  7419  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlemlim  7437  cauappcvgpr  7438  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemcl  7452  caucvgpr  7458  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemopu  7475  caucvgprpr  7488  suplocexpr  7501  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  lttrsr  7538  recexgt0sr  7549  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  caucvgsr  7578  suplocsrlem  7584  ltresr  7615  pitonn  7624  peano1nnnn  7628  peano2nnnn  7629  axprecex  7656  axcnre  7657  axpre-lttrn  7660  peano5nnnn  7668  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  axlttrn  7801  axsuploc  7805  letri3  7813  letr  7815  le2add  8174  lt2add  8175  ltleadd  8176  lt2sub  8190  le2sub  8191  apreap  8316  apreim  8332  apti  8351  msq11  8624  dfinfre  8678  sup3exmid  8679  cju  8683  peano5nni  8687  1nn  8695  peano2nn  8696  nn2ge  8717  nominpos  8915  elz2  9080  dfuzi  9119  uzind  9120  supinfneg  9346  infsupneg  9347  xrletri3  9543  xrletr  9546  z2ge  9564  elixx1  9635  elioo2  9659  iooshf  9690  iooneg  9726  iccneg  9727  icoshft  9728  elfz1  9750  fzdifsuc  9816  fzrev  9819  1fv  9871  exbtwnzlemstep  9980  exbtwnzlemshrink  9981  exbtwnzlemex  9982  exbtwnz  9983  rebtwn2zlemstep  9985  rebtwn2zlemshrink  9986  rebtwn2z  9987  qbtwnre  9989  qbtwnxr  9990  flval  10000  flqlelt  10004  flqbi  10018  flqbi2  10019  modqid2  10079  q2submod  10113  nnesq  10366  hashunlem  10505  zfz1isolem1  10538  zfz1iso  10539  seq3coll  10540  shftlem  10543  shftfibg  10547  shftfib  10550  shftfn  10551  2shfti  10558  cjval  10572  cjth  10573  remim  10587  caucvgrelemcau  10707  caucvgre  10708  cvg1nlemcau  10711  cvg1nlemres  10712  rexanuz2  10718  recvguniq  10722  resqrexlemgt0  10747  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemsqa  10751  resqrexlemex  10752  rsqrmo  10754  resqrtcl  10756  rersqrtthlem  10757  absdiflt  10819  absdifle  10820  cau3lem  10841  icodiamlt  10907  maxleast  10940  negfi  10954  minmax  10956  lemininf  10960  ltmininf  10961  xrmaxlesup  10983  xrminmax  10989  xrltmininf  10994  xrlemininf  10995  iooinsup  11001  clim  11005  clim2  11007  climshftlemg  11026  addcn2  11034  climcau  11071  summodc  11107  fsum3  11111  fsum2dlemstep  11158  fisumcom2  11162  fsum00  11186  sin01bnd  11378  cos01bnd  11379  divalgmod  11536  ndvdssub  11539  zsupcllemstep  11550  infssuzex  11554  gcdsupex  11558  gcdsupcl  11559  gcddvds  11564  dvdslegcd  11565  bezoutlemmain  11598  bezoutlemex  11601  bezoutlemzz  11602  bezoutlemeu  11607  bezoutlemle  11608  bezoutlemsup  11609  dfgcd3  11610  dfgcd2  11614  gcddiv  11619  lcmval  11656  lcmcllem  11660  dvdslcm  11662  lcmledvds  11663  lcmgcdlem  11670  lcmdvds  11672  coprmgcdb  11681  ncoprmgcdne1b  11682  coprmdvds1  11684  qredeu  11690  divgcdcoprm0  11694  divgcdcoprmex  11695  isprm3  11711  pw2dvdslemn  11754  pw2dvdseu  11757  oddpwdclemxy  11758  qnumdencl  11776  qnumdenbi  11781  crth  11811  ennnfonelemim  11848  exmidunben  11850  ctinfom  11852  ctiunctlemu1st  11858  ctiunctlemu2nd  11859  ctiunctlemudc  11861  ctiunctlemfo  11863  istopg  12077  fiinbas  12127  eltg2  12133  topbas  12147  neiint  12225  neipsm  12234  opnneissb  12235  opnssneib  12236  innei  12243  restbasg  12248  iscnp4  12298  cnpnei  12299  cnconst2  12313  cnptopresti  12318  cnptoprest  12319  cnpdis  12322  lmss  12326  lmres  12328  txbas  12338  eltx  12339  neitx  12348  txcnp  12351  txcnmpt  12353  uptx  12354  txdis  12357  txdis1cn  12358  txlm  12359  txhmeo  12399  ispsmet  12403  ismet  12424  isxmet  12425  bldisj  12481  blininf  12504  blssexps  12509  blssex  12510  ssblex  12511  xmspropd  12557  mspropd  12558  neibl  12571  metequiv  12575  bdmopn  12584  metrest  12586  xmetxp  12587  xmetxpbl  12588  xmettx  12590  metcnp3  12591  tgioo  12626  tgqioo  12627  addcncntoplem  12631  mulcncflem  12670  dedekindeu  12681  dedekindicclemicc  12690  limccl  12708  ellimc3apf  12709  limcimolemlt  12713  limccoap  12727  sin0pilem2  12774  sincosq1sgn  12818  sincosq2sgn  12819  sincosq3sgn  12820  sincosq4sgn  12821  bj-sseq  12895  bj-nalset  12989  bj-indeq  13023  bj-2inf  13032  subctctexmid  13092  exmidsbthrlem  13113  sbthom  13117  qdencn  13118
  Copyright terms: Public domain W3C validator