ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi12d Unicode 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  |-  ( 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 453 . 2  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
3 anbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43anbi2d 452 . 2  |-  ( ph  ->  ( ( ch  /\  th )  <->  ( ch  /\  ta ) ) )
52, 4bitrd 186 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
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  844  orbididc  895  3anbi123d  1244  xorbi2d  1312  xorbi1d  1313  drsb1  1721  mopick  2020  clelab  2204  cbvrexf  2573  cbvreu  2576  cbvrexdva2  2583  cbvrab  2600  gencbvex  2646  rspce  2697  eqvincf  2721  ceqsrexv  2726  elrabf  2748  rexab2  2759  reu2  2781  reu6  2782  rmo4  2786  reu8  2789  reuind  2796  sbcan  2857  sbcang  2858  sbcabel  2896  rmob  2907  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  difjust  2975  injust  2979  eldif  2983  ssconb  3106  elin  3156  opeq1  3578  opeq2  3579  2ralunsn  3598  elunii  3614  csbunig  3617  eluniab  3621  cbvopab  3857  cbvopab1  3859  cbvopab2  3860  cbvopab1s  3861  cbvopab2v  3863  cbvmpt  3880  trel  3890  nalset  3916  elssabg  3931  mss  3989  exss  3990  opelopab2a  4028  poeq1  4062  pocl  4066  soeq1  4078  weeq1  4119  weeq2  4120  ordeq  4135  zfun  4197  snnex  4207  reusv3  4218  ontr2exmid  4276  regexmid  4286  onintexmid  4323  reg3exmid  4330  peano5  4347  limom  4362  nnregexmid  4368  vtoclr  4414  opeliunxp  4421  poinxp  4435  opbrop  4445  csbxpg  4447  opeliunxp2  4504  relop  4514  brcogw  4532  elrnmpt1  4613  elsnres  4675  dfres2  4688  inimasn  4771  xpcanm  4790  xpcan2m  4791  elxp4  4838  elxp5  4839  cnvsom  4891  sbcfung  4955  funopg  4964  fununi  4998  funcnvuni  4999  fneq1  5018  2elresin  5041  feq1  5061  sbcfng  5075  sbcfg  5076  f1eq1  5118  foeq1  5133  f1oeq1  5148  f1oeq2  5149  f1oeq3  5150  ffoss  5189  brprcneu  5202  fv3  5229  tz6.12f  5234  ssimaex  5266  fvopab3g  5277  fvopab3ig  5278  fvopab6  5296  fmptco  5362  elunirn  5437  f1imaeq  5446  foeqcnvco  5461  fliftfun  5467  fliftval  5471  isoeq1  5472  isoeq4  5475  isoini  5488  isopolem  5492  f1oiso2  5497  riotabidv  5501  cbvriota  5509  acexmid  5542  cbvoprab1  5607  cbvoprab2  5608  cbvoprab12  5609  cbvmpt2x  5613  ov  5651  ovig  5653  ovg  5670  caovimo  5725  caoftrn  5767  opabex3d  5779  opabex3  5780  elxp6  5827  unielxp  5831  dfoprab4  5849  dfoprab4f  5850  fmpt2x  5857  xporderlem  5883  poxp  5884  cnvoprab  5886  f1od2  5887  sprmpt2  5891  isprmpt2  5892  dftpos4  5912  tpostpos  5913  smoiso  5951  tfrlem3ag  5958  tfrlem3a  5959  tfr0dm  5971  tfrlemisucaccv  5974  tfrlemiex  5980  tfrlemi1  5981  tfrlemi14d  5982  tfrexlem  5983  tfr1onlem3ag  5986  tfr1onlemsucaccv  5990  tfr1onlemex  5996  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllemex  6009  tfrcllemaccex  6010  tfrcllemres  6011  tfrcldm  6012  frec0g  6046  frecabcl  6048  freccllem  6051  frecfcllem  6053  frecsuclem  6055  frecsuc  6056  nnacan  6151  nnmcan  6158  nnaordex  6166  ertr  6187  brecop  6262  eroveu  6263  ecopovtrn  6269  ecopovtrng  6272  th3qlem1  6274  th3qlem2  6275  th3q  6277  xpsnen  6365  endisj  6368  xpf1o  6385  phplem3g  6391  ssfiexmid  6411  domfiexmid  6413  findcard2s  6424  ac6sfi  6431  f1dmvrnfibi  6452  supeq1  6458  supeq3  6462  supeq123d  6463  supmoti  6465  eqsupti  6468  supsnti  6477  isotilem  6478  isoti  6479  supisolem  6480  supisoex  6481  cnvinfex  6490  cnvti  6491  eqinfti  6492  infvalti  6494  ltsopi  6572  recexnq  6642  recmulnqg  6643  ltsonq  6650  lt2addnq  6656  lt2mulnq  6657  ltbtwnnqq  6667  prarloclemarch2  6671  enq0sym  6684  enq0ref  6685  enq0tr  6686  enq0breq  6688  addnq0mo  6699  mulnq0mo  6700  addnnnq0  6701  mulnnnq0  6702  nqnq0a  6706  nqnq0m  6707  elinp  6726  prcdnql  6736  prcunqu  6737  prltlu  6739  prdisj  6744  prarloclemlo  6746  prarloclem3  6749  prarloclem5  6752  ltdfpr  6758  genprndl  6773  genprndu  6774  genpdisj  6775  appdivnq  6815  ltpopr  6847  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  ltexpri  6865  recexprlemm  6876  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  recexpr  6890  aptiprleml  6891  archpr  6895  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlemlim  6913  cauappcvgpr  6914  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemcl  6928  caucvgpr  6934  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemopu  6951  caucvgprpr  6964  addsrmo  6982  mulsrmo  6983  addsrpr  6984  mulsrpr  6985  lttrsr  7001  recexgt0sr  7012  caucvgsrlemcau  7031  caucvgsrlemgt1  7033  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  caucvgsr  7040  ltresr  7069  pitonn  7078  peano1nnnn  7082  peano2nnnn  7083  axprecex  7108  axcnre  7109  axpre-lttrn  7112  peano5nnnn  7120  axcaucvglemcau  7126  axcaucvglemres  7127  axlttrn  7248  letri3  7259  letr  7261  le2add  7615  lt2add  7616  ltleadd  7617  lt2sub  7631  le2sub  7632  apreap  7754  apreim  7770  apti  7789  msq11  8047  dfinfre  8101  cju  8105  peano5nni  8109  1nn  8117  peano2nn  8118  nn2ge  8138  nominpos  8335  elz2  8500  dfuzi  8538  uzind  8539  supinfneg  8764  infsupneg  8765  xrletri3  8951  xrletr  8954  z2ge  8969  elixx1  8996  elioo2  9020  iooshf  9051  iooneg  9086  iccneg  9087  icoshft  9088  elfz1  9110  fzdifsuc  9174  fzrev  9177  1fv  9226  exbtwnzlemstep  9334  exbtwnzlemshrink  9335  exbtwnzlemex  9336  exbtwnz  9337  rebtwn2zlemstep  9339  rebtwn2zlemshrink  9340  rebtwn2z  9341  qbtwnre  9343  qbtwnxr  9344  flval  9354  flqlelt  9358  flqbi  9372  flqbi2  9373  modqid2  9433  q2submod  9467  nnesq  9689  sizeunlem  9828  shftlem  9842  shftfibg  9846  shftfib  9849  shftfn  9850  2shfti  9857  cjval  9870  cjth  9871  remim  9885  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemcau  10008  cvg1nlemres  10009  rexanuz2  10015  recvguniq  10019  resqrexlemgt0  10044  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemsqa  10048  resqrexlemex  10049  rsqrmo  10051  resqrtcl  10053  rersqrtthlem  10054  absdiflt  10116  absdifle  10117  cau3lem  10138  icodiamlt  10204  maxleast  10237  negfi  10248  minmax  10250  lemininf  10253  ltmininf  10254  clim  10258  clim2  10260  climshftlemg  10279  addcn2  10287  climcau  10322  divalgmod  10471  ndvdssub  10474  zsupcllemstep  10485  infssuzex  10489  gcdsupex  10493  gcdsupcl  10494  gcddvds  10499  dvdslegcd  10500  bezoutlemmain  10531  bezoutlemex  10534  bezoutlemzz  10535  bezoutlemeu  10540  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  dfgcd2  10547  gcddiv  10552  lcmval  10589  lcmcllem  10593  dvdslcm  10595  lcmledvds  10596  lcmgcdlem  10603  lcmdvds  10605  coprmgcdb  10614  ncoprmgcdne1b  10615  coprmdvds1  10617  qredeu  10623  divgcdcoprm0  10627  divgcdcoprmex  10628  isprm3  10644  pw2dvdslemn  10687  pw2dvdseu  10690  oddpwdclemxy  10691  bj-sseq  10753  bj-nalset  10844  bj-indeq  10882  bj-2inf  10891  qdencn  10943
  Copyright terms: Public domain W3C validator