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

Theorem anbi12d 450
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 446 . 2  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
3 anbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43anbi2d 445 . 2  |-  ( ph  ->  ( ( ch  /\  th )  <->  ( ch  /\  ta ) ) )
52, 4bitrd 181 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm4.38  545  pm5.17dc  819  orbididc  869  3anbi123d  1216  xorbi2d  1285  xorbi1d  1286  drsb1  1694  mopick  1992  clelab  2176  cbvrexf  2543  cbvreu  2546  cbvrexdva2  2553  cbvrab  2570  gencbvex  2615  rspce  2666  eqvincf  2689  ceqsrexv  2694  elrabf  2716  rexab2  2727  reu2  2749  reu6  2750  rmo4  2754  reu8  2757  reuind  2764  sbcan  2825  sbcang  2826  sbcabel  2864  rmob  2875  cbvrexcsf  2934  cbvreucsf  2935  cbvrabcsf  2936  difjust  2944  injust  2948  eldif  2952  psseq1  3056  psseq2  3057  ssconb  3101  elin  3151  opeq1  3574  opeq2  3575  2ralunsn  3594  elunii  3610  csbunig  3613  eluniab  3617  cbvopab  3853  cbvopab1  3855  cbvopab2  3856  cbvopab1s  3857  cbvopab2v  3859  cbvmpt  3876  trel  3886  nalset  3912  elssabg  3927  mss  3987  exss  3988  opelopab2a  4027  poeq1  4061  pocl  4065  soeq1  4077  weeq1  4118  weeq2  4119  ordeq  4134  zfun  4196  snnex  4206  reusv3  4217  ontr2exmid  4275  regexmid  4285  onintexmid  4322  reg3exmid  4329  peano5  4346  limom  4361  nnregexmid  4367  vtoclr  4413  opeliunxp  4420  poinxp  4434  opbrop  4444  csbxpg  4446  opeliunxp2  4501  relop  4511  brcogw  4529  elrnmpt1  4610  elsnres  4672  dfres2  4683  inimasn  4766  xpcanm  4785  xpcan2m  4786  elxp4  4833  elxp5  4834  cnvsom  4886  sbcfung  4950  funopg  4959  fununi  4992  funcnvuni  4993  fneq1  5012  2elresin  5035  feq1  5055  sbcfng  5069  sbcfg  5070  f1eq1  5112  foeq1  5127  f1oeq1  5142  f1oeq2  5143  f1oeq3  5144  ffoss  5183  brprcneu  5196  fv3  5222  tz6.12f  5227  ssimaex  5259  fvopab3g  5270  fvopab3ig  5271  fvopab6  5289  fmptco  5355  elunirn  5430  f1imaeq  5439  f1imapss  5440  foeqcnvco  5455  fliftfun  5461  fliftval  5465  isoeq1  5466  isoeq4  5469  isoini  5482  isopolem  5486  f1oiso2  5491  riotabidv  5495  cbvriota  5503  acexmid  5536  cbvoprab1  5601  cbvoprab2  5602  cbvoprab12  5603  cbvmpt2x  5607  ov  5645  ovig  5647  ovg  5664  caovimo  5719  caoftrn  5761  opabex3d  5773  opabex3  5774  elxp6  5821  unielxp  5825  dfoprab4  5843  dfoprab4f  5844  fmpt2x  5851  xporderlem  5877  poxp  5878  cnvoprab  5880  f1od2  5881  sprmpt2  5885  isprmpt2  5886  dftpos4  5906  tpostpos  5907  smoiso  5945  tfrlem3ag  5952  tfrlem3a  5953  tfr0  5965  tfrlemisucaccv  5967  tfrlemiex  5973  tfrlemi1  5974  tfrlemi14d  5975  tfrexlem  5976  frec0g  6011  frecsuclem3  6018  frecsuc  6019  nnacan  6113  nnmcan  6120  nnaordex  6128  ertr  6149  brecop  6224  eroveu  6225  ecopovtrn  6231  ecopovtrng  6234  th3qlem1  6236  th3qlem2  6237  th3q  6239  xpsnen  6323  endisj  6326  phplem3g  6347  ssfiexmid  6364  findcard2s  6375  ac6sfi  6380  ltsopi  6446  recexnq  6516  recmulnqg  6517  ltsonq  6524  lt2addnq  6530  lt2mulnq  6531  ltbtwnnqq  6541  prarloclemarch2  6545  enq0sym  6558  enq0ref  6559  enq0tr  6560  enq0breq  6562  addnq0mo  6573  mulnq0mo  6574  addnnnq0  6575  mulnnnq0  6576  nqnq0a  6580  nqnq0m  6581  elinp  6600  prcdnql  6610  prcunqu  6611  prltlu  6613  prdisj  6618  prarloclemlo  6620  prarloclem3  6623  prarloclem5  6626  ltdfpr  6632  genprndl  6647  genprndu  6648  genpdisj  6649  appdivnq  6689  ltpopr  6721  ltexprlemdisj  6732  ltexprlemloc  6733  ltexprlemrl  6736  ltexprlemru  6738  ltexpri  6739  recexprlemm  6750  recexprlemdisj  6756  recexprlemloc  6757  recexprlem1ssl  6759  recexprlem1ssu  6760  recexpr  6764  aptiprleml  6765  archpr  6769  cauappcvgprlemladdru  6782  cauappcvgprlemladdrl  6783  cauappcvgprlem1  6785  cauappcvgprlemlim  6787  cauappcvgpr  6788  caucvgprlemnkj  6792  caucvgprlemnbj  6793  caucvgprlemcl  6802  caucvgpr  6808  caucvgprprlemcbv  6813  caucvgprprlemval  6814  caucvgprprlemopu  6825  caucvgprpr  6838  addsrmo  6856  mulsrmo  6857  addsrpr  6858  mulsrpr  6859  lttrsr  6875  recexgt0sr  6886  caucvgsrlemcau  6905  caucvgsrlemgt1  6907  caucvgsrlemoffcau  6910  caucvgsrlemoffres  6912  caucvgsr  6914  ltresr  6943  pitonn  6952  peano1nnnn  6956  peano2nnnn  6957  axprecex  6982  axcnre  6983  axpre-lttrn  6986  peano5nnnn  6994  axcaucvglemcau  7000  axcaucvglemres  7001  axlttrn  7117  letri3  7128  letr  7130  le2add  7483  lt2add  7484  ltleadd  7485  lt2sub  7499  le2sub  7500  apreap  7622  apreim  7638  apti  7657  msq11  7913  cju  7959  peano5nni  7963  1nn  7971  peano2nn  7972  nn2ge  7992  nominpos  8189  elz2  8340  dfuzi  8377  uzind  8378  xrletri3  8792  xrletr  8795  z2ge  8810  elixx1  8837  elioo2  8861  iooshf  8892  iooneg  8927  iccneg  8928  icoshft  8929  elfz1  8951  fzdifsuc  9015  fzrev  9018  1fv  9068  qbtwnzlemstep  9175  qbtwnzlemshrink  9176  qbtwnzlemex  9177  qbtwnz  9178  rebtwn2zlemstep  9179  rebtwn2zlemshrink  9180  rebtwn2z  9181  qbtwnre  9183  flval  9189  flqlelt  9191  flqbi  9205  flqbi2  9206  modqid2  9266  q2submod  9300  nnesq  9500  shftlem  9609  shftfibg  9613  shftfib  9616  shftfn  9617  2shfti  9624  cjval  9637  cjth  9638  remim  9652  caucvgrelemcau  9771  caucvgre  9772  cvg1nlemcau  9775  cvg1nlemres  9776  rexanuz2  9781  recvguniq  9785  resqrexlemgt0  9810  resqrexlemoverl  9811  resqrexlemglsq  9812  resqrexlemsqa  9814  resqrexlemex  9815  rsqrmo  9817  resqrtcl  9819  rersqrtthlem  9820  absdiflt  9882  absdifle  9883  cau3lem  9904  icodiamlt  9970  clim  9996  clim2  9998  climshftlemg  10017  addcn2  10025  climcau  10060  sumeq1  10068  pw2dvdslemn  10196  pw2dvdseu  10199  oddpwdclemxy  10200  bj-sseq  10261  bj-nalset  10345  bj-indeq  10383  bj-2inf  10392  qdencn  10454
  Copyright terms: Public domain W3C validator