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  594  pm5.17dc  889  orbididc  937  3anbi123d  1290  xorbi2d  1358  xorbi1d  1359  drsb1  1771  mopick  2077  clelab  2265  cbvrexf  2649  cbvreu  2652  cbvrexdva2  2662  cbvrab  2684  gencbvex  2732  rspce  2784  eqvincf  2810  ceqsrexv  2815  elrabf  2838  rexab2  2850  reu2  2872  reu6  2873  rmo4  2877  reu8  2880  reuind  2889  sbcan  2951  sbcang  2952  sbcabel  2990  rmob  3001  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  difjust  3072  injust  3076  eldif  3080  ssconb  3209  elin  3259  opeq1  3705  opeq2  3706  2ralunsn  3725  elunii  3741  csbunig  3744  eluniab  3748  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab2v  4005  cbvmptf  4022  cbvmpt  4023  trel  4033  nalset  4058  elssabg  4073  mss  4148  exss  4149  opelopab2a  4187  poeq1  4221  pocl  4225  soeq1  4237  weeq1  4278  weeq2  4279  ordeq  4294  zfun  4356  snnex  4369  reusv3  4381  ontr2exmid  4440  regexmid  4450  onintexmid  4487  reg3exmid  4494  peano5  4512  limom  4527  nnregexmid  4534  vtoclr  4587  opeliunxp  4594  poinxp  4608  opbrop  4618  csbxpg  4620  opeliunxp2  4679  relop  4689  brcogw  4708  elrnmpt1  4790  elsnres  4856  dfres2  4871  inimasn  4956  xpcanm  4978  xpcan2m  4979  elxp4  5026  elxp5  5027  cnvsom  5082  sbcfung  5147  funopg  5157  fununi  5191  funcnvuni  5192  fneq1  5211  2elresin  5234  feq1  5255  sbcfng  5270  sbcfg  5271  f1eq1  5323  foeq1  5341  f1oeq1  5356  f1oeq2  5357  f1oeq3  5358  ffoss  5399  brprcneu  5414  fv3  5444  tz6.12f  5450  ssimaex  5482  fvopab3g  5494  fvopab3ig  5495  fvopab6  5517  fmptco  5586  elunirn  5667  f1imaeq  5676  foeqcnvco  5691  fliftfun  5697  fliftval  5701  isoeq1  5702  isoeq4  5705  isoini  5719  isopolem  5723  f1oiso2  5728  riotabidv  5732  cbvriota  5740  acexmid  5773  ovanraleqv  5798  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvmpox  5849  ov  5890  ovig  5892  ovg  5909  caovimo  5964  caoftrn  6007  opabex3d  6019  opabex3  6020  elxp6  6067  unielxp  6072  dfoprab4  6090  dfoprab4f  6091  fmpox  6098  xporderlem  6128  poxp  6129  cnvoprab  6131  f1od2  6132  opeliunxp2f  6135  rbropapd  6139  dftpos4  6160  tpostpos  6161  smoiso  6199  tfrlem3ag  6206  tfrlem3a  6207  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemiex  6228  tfrlemi1  6229  tfrlemi14d  6230  tfrexlem  6231  tfr1onlem3ag  6234  tfr1onlemsucaccv  6238  tfr1onlemex  6244  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemex  6257  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  frec0g  6294  frecabcl  6296  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnacan  6408  nnmcan  6415  nnaordex  6423  ertr  6444  brecop  6519  eroveu  6520  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  th3qlem2  6532  th3q  6534  elpm2r  6560  mapsncnv  6589  elixp2  6596  ixpeq1  6603  elixpsn  6629  ixpsnf1o  6630  mapsnen  6705  map1  6706  xpsnen  6715  endisj  6718  xpf1o  6738  phplem3g  6750  ssfiexmid  6770  domfiexmid  6772  findcard2s  6784  isinfinf  6791  ac6sfi  6792  fiintim  6817  fisseneq  6820  f1dmvrnfibi  6832  sbthlem2  6846  isbth  6855  supeq1  6873  supeq3  6877  supeq123d  6878  supmoti  6880  eqsupti  6883  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  cnvinfex  6905  cnvti  6906  eqinfti  6907  infvalti  6909  updjud  6967  ctssexmid  7024  omniwomnimkv  7039  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  acfun  7068  ccfunen  7084  cc2lem  7086  cc3  7088  ltsopi  7140  recexnq  7210  recmulnqg  7211  ltsonq  7218  lt2addnq  7224  lt2mulnq  7225  ltbtwnnqq  7235  prarloclemarch2  7239  enq0sym  7252  enq0ref  7253  enq0tr  7254  enq0breq  7256  addnq0mo  7267  mulnq0mo  7268  addnnnq0  7269  mulnnnq0  7270  nqnq0a  7274  nqnq0m  7275  elinp  7294  prcdnql  7304  prcunqu  7305  prltlu  7307  prdisj  7312  prarloclemlo  7314  prarloclem3  7317  prarloclem5  7320  ltdfpr  7326  genprndl  7341  genprndu  7342  genpdisj  7343  appdivnq  7383  ltpopr  7415  ltexprlemdisj  7426  ltexprlemloc  7427  ltexprlemrl  7430  ltexprlemru  7432  ltexpri  7433  recexprlemm  7444  recexprlemdisj  7450  recexprlemloc  7451  recexprlem1ssl  7453  recexprlem1ssu  7454  recexpr  7458  aptiprleml  7459  archpr  7463  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  cauappcvgprlem1  7479  cauappcvgprlemlim  7481  cauappcvgpr  7482  caucvgprlemnkj  7486  caucvgprlemnbj  7487  caucvgprlemcl  7496  caucvgpr  7502  caucvgprprlemcbv  7507  caucvgprprlemval  7508  caucvgprprlemopu  7519  caucvgprpr  7532  suplocexpr  7545  addsrmo  7563  mulsrmo  7564  addsrpr  7565  mulsrpr  7566  lttrsr  7582  recexgt0sr  7593  caucvgsrlemcau  7613  caucvgsrlemgt1  7615  caucvgsrlemoffcau  7618  caucvgsrlemoffres  7620  caucvgsr  7622  suplocsrlem  7628  ltresr  7659  pitonn  7668  peano1nnnn  7672  peano2nnnn  7673  axprecex  7700  axcnre  7701  axpre-lttrn  7704  peano5nnnn  7712  axcaucvglemcau  7718  axcaucvglemres  7719  axpre-suploclemres  7721  axpre-suploc  7722  axlttrn  7845  axsuploc  7849  letri3  7857  letr  7859  le2add  8218  lt2add  8219  ltleadd  8220  lt2sub  8234  le2sub  8235  apreap  8361  apreim  8377  apti  8396  msq11  8672  dfinfre  8726  sup3exmid  8727  cju  8731  peano5nni  8735  1nn  8743  peano2nn  8744  nn2ge  8765  nominpos  8969  elz2  9134  dfuzi  9173  uzind  9174  supinfneg  9402  infsupneg  9403  xrletri3  9600  xrletr  9603  z2ge  9621  elixx1  9692  elioo2  9716  iooshf  9747  iooneg  9783  iccneg  9784  icoshft  9785  elfz1  9807  fzdifsuc  9873  fzrev  9876  1fv  9928  exbtwnzlemstep  10037  exbtwnzlemshrink  10038  exbtwnzlemex  10039  exbtwnz  10040  rebtwn2zlemstep  10042  rebtwn2zlemshrink  10043  rebtwn2z  10044  qbtwnre  10046  qbtwnxr  10047  flval  10057  flqlelt  10061  flqbi  10075  flqbi2  10076  modqid2  10136  q2submod  10170  nnesq  10423  hashunlem  10562  zfz1isolem1  10595  zfz1iso  10596  seq3coll  10597  shftlem  10600  shftfibg  10604  shftfib  10607  shftfn  10608  2shfti  10615  cjval  10629  cjth  10630  remim  10644  caucvgrelemcau  10764  caucvgre  10765  cvg1nlemcau  10768  cvg1nlemres  10769  rexanuz2  10775  recvguniq  10779  resqrexlemgt0  10804  resqrexlemoverl  10805  resqrexlemglsq  10806  resqrexlemsqa  10808  resqrexlemex  10809  rsqrmo  10811  resqrtcl  10813  rersqrtthlem  10814  absdiflt  10876  absdifle  10877  cau3lem  10898  icodiamlt  10964  maxleast  10997  negfi  11011  minmax  11013  lemininf  11017  ltmininf  11018  xrmaxlesup  11040  xrminmax  11046  xrltmininf  11051  xrlemininf  11052  iooinsup  11058  clim  11062  clim2  11064  climshftlemg  11083  addcn2  11091  climcau  11128  summodc  11164  fsum3  11168  fsum2dlemstep  11215  fisumcom2  11219  fsum00  11243  ntrivcvgap0  11330  prodeq1f  11333  prodeq2w  11337  prodeq2  11338  prodmodc  11359  sin01bnd  11475  cos01bnd  11476  divalgmod  11635  ndvdssub  11638  zsupcllemstep  11649  infssuzex  11653  gcdsupex  11657  gcdsupcl  11658  gcddvds  11663  dvdslegcd  11664  bezoutlemmain  11697  bezoutlemex  11700  bezoutlemzz  11701  bezoutlemeu  11706  bezoutlemle  11707  bezoutlemsup  11708  dfgcd3  11709  dfgcd2  11713  gcddiv  11718  lcmval  11755  lcmcllem  11759  dvdslcm  11761  lcmledvds  11762  lcmgcdlem  11769  lcmdvds  11771  coprmgcdb  11780  ncoprmgcdne1b  11781  coprmdvds1  11783  qredeu  11789  divgcdcoprm0  11793  divgcdcoprmex  11794  isprm3  11810  pw2dvdslemn  11854  pw2dvdseu  11857  oddpwdclemxy  11858  qnumdencl  11876  qnumdenbi  11881  crth  11911  ennnfonelemim  11948  exmidunben  11950  ctinfom  11952  ctiunctlemu1st  11958  ctiunctlemu2nd  11959  ctiunctlemudc  11961  ctiunctlemfo  11963  istopg  12180  fiinbas  12230  eltg2  12236  topbas  12250  neiint  12328  neipsm  12337  opnneissb  12338  opnssneib  12339  innei  12346  restbasg  12351  iscnp4  12401  cnpnei  12402  cnconst2  12416  cnptopresti  12421  cnptoprest  12422  cnpdis  12425  lmss  12429  lmres  12431  txbas  12441  eltx  12442  neitx  12451  txcnp  12454  txcnmpt  12456  uptx  12457  txdis  12460  txdis1cn  12461  txlm  12462  txhmeo  12502  ispsmet  12506  ismet  12527  isxmet  12528  bldisj  12584  blininf  12607  blssexps  12612  blssex  12613  ssblex  12614  xmspropd  12660  mspropd  12661  neibl  12674  metequiv  12678  bdmopn  12687  metrest  12689  xmetxp  12690  xmetxpbl  12691  xmettx  12693  metcnp3  12694  tgioo  12729  tgqioo  12730  addcncntoplem  12734  mulcncflem  12773  dedekindeu  12784  dedekindicclemicc  12793  limccl  12811  ellimc3apf  12812  limcimolemlt  12816  limccoap  12830  sin0pilem2  12885  sincosq1sgn  12929  sincosq2sgn  12930  sincosq3sgn  12931  sincosq4sgn  12932  bj-sseq  13058  bj-nalset  13152  bj-indeq  13186  bj-2inf  13195  subctctexmid  13255  exmidsbthrlem  13278  sbthom  13282  qdencn  13283
  Copyright terms: Public domain W3C validator