MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi1d Unicode version

Theorem anbi1d 686
Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
bid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
anbi1d  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )

Proof of Theorem anbi1d
StepHypRef Expression
1 bid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 23 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 622 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi1  688  anbi12d  692  bi2anan9  844  pm5.71  903  cador  1397  drsb1  2057  eleq1  2449  rexeqf  2846  reueq1f  2847  rmoeq1f  2848  rabeqf  2894  vtocl2gaf  2963  alexeq  3010  ceqex  3011  elrabi  3035  sbc2or  3114  sbc5  3130  rexss  3355  psstr  3396  ineq1  3480  difin2  3548  r19.28z  3665  r19.28zv  3668  ssunsn2  3903  preq12bg  3921  opeq1  3928  eluni  3962  disjxun  4153  mpteq12f  4228  axrep1  4264  axrep2  4265  axrep3  4266  zfrepclf  4269  axsep  4272  axsep2  4274  zfauscl  4275  opthg  4379  copsexg  4385  euotd  4400  elopab  4405  pocl  4453  dflim2  4580  uniuni  4658  reusv2lem4  4669  rabxfrd  4686  limuni3  4774  xpeq1  4834  elxpi  4836  vtoclr  4864  opbrop  4897  opelresg  5095  resopab2  5132  elxp4  5299  elxp5  5300  fun11  5458  feq2  5519  f1eq2  5577  f1eq3  5578  foeq2  5592  brprcneu  5663  ssimaexg  5730  dmfco  5738  fndmdif  5775  rexsupp  5796  respreima  5800  opabex3d  5930  opabex3  5931  isoeq5  5984  isoini  5999  isopolem  6006  f1oiso  6012  f1oiso2  6013  oprabid  6046  mpt2eq123  6074  mpt2eq123dva  6076  eloprabga  6101  resoprab  6107  resoprab2  6108  ov  6134  ov3  6151  ov6g  6152  ovg  6153  caoftrn  6280  eloprabi  6354  cnvf1o  6386  frxp  6394  xporderlem  6395  poxp  6396  fnwelem  6399  opiota  6473  riotaeqdv  6488  smoel2  6563  omeu  6766  oeeui  6783  omabs  6828  omopth  6839  qliftel  6925  brecop  6935  eroveu  6937  erov  6939  ecopovtrn  6945  th3qlem2  6949  th3q  6951  ixpsnf1o  7040  dom2lem  7085  xpsnen  7130  xpassen  7140  pw2f1olem  7150  xpf1o  7207  unxpdom  7254  domunfican  7317  preleq  7507  zfinf  7529  cantnfs  7556  tcvalg  7612  r0weon  7829  fseqenlem1  7840  acni2  7862  aceq1  7933  aceq0  7934  dfac2a  7945  dfac12lem2  7959  cardcf  8067  cfeq0  8071  cfsuc  8072  cff1  8073  cfss  8080  isf32lem5  8172  fin1a2lem6  8220  zfac  8275  brdom7disj  8344  brdom6disj  8345  axrepnd  8404  axunndlem1  8405  axinfnd  8416  axacndlem5  8421  axacnd  8422  zfcndrep  8424  zfcndinf  8428  zfcndac  8429  pwfseqlem4a  8471  pwfseqlem4  8472  gruina  8628  grothomex  8639  ordpipq  8754  elnpi  8800  genpass  8821  ltprord  8842  reclem2pr  8860  reclem3pr  8861  recexpr  8863  ltsosr  8904  mulgt0sr  8915  supsr  8922  ltresr  8950  axpre-lttrn  8976  axpre-mulgt0  8978  prime  10284  peano5uzti  10293  uzindOLD  10298  rexuz  10461  ltxr  10649  qbtwnre  10719  xmulneg1  10782  supxr2  10826  ixxval  10858  fzval  10979  nn0opth2  11494  hashbclem  11630  hashf1lem2  11634  abslt  12047  absle  12048  lenegsq  12053  abs2difabs  12067  ello12  12239  elo12  12250  o1lo1  12260  rlimuni  12273  lo1resb  12287  o1resb  12289  2clim  12295  rlimcn2  12313  climcn2  12315  addcn2  12316  mulcn2  12318  o1of2  12335  sumeq1f  12411  fsum2dlem  12483  znnenlem  12740  nndivdvds  12787  divalg2  12854  smupval  12929  gcdval  12937  gcdass  12974  rpexp  13049  pythagtriplem2  13120  pythagtrip  13137  vdwapun  13271  0ram  13317  ramub1lem2  13324  pwsle  13643  imasleval  13695  ismre  13744  ismri  13785  iscatd2  13835  isssc  13949  funcpropd  14026  fullpropd  14046  fthres2b  14056  fthres2c  14057  setcsect  14173  prslem  14317  drsdir  14321  posi  14336  tosso  14394  ipoval  14509  ipolt  14514  odudlatb  14551  dirge  14611  mndpropd  14650  mhmpropd  14673  issubg3  14889  isga  14997  isslw  15171  dprdw  15497  subgdmdprd  15521  drngpropd  15791  issubrg  15797  islmod  15883  lmodlema  15884  lmodprop2d  15935  lsslss  15966  lbspropd  16100  lbsacsbs  16157  aspval2  16334  psrbag  16360  znleval  16760  istopg  16893  basis2  16941  tg2  16955  iscld  17016  neival  17091  isnei  17092  isneip  17094  neiptoptop  17120  neiptopnei  17121  neitr  17168  restlp  17171  iscn  17223  cnpval  17224  iscnp  17225  regsep  17322  nrmsep3  17343  1stcclb  17430  2ndc1stc  17437  2ndcctbss  17441  2ndcdisj  17442  llyi  17460  nllyi  17461  hausmapdom  17486  elkgen  17491  txbas  17522  txcls  17559  txcnpi  17563  ptpjopn  17567  txdis1cn  17590  txtube  17595  txcmplem1  17596  hausdiag  17600  tx1stc  17605  txkgen  17607  xkococnlem  17614  xkococn  17615  elqtop  17652  kqreglem1  17696  elmptrab  17782  isfbas  17784  elflim2  17919  elflim  17926  hauspwpwf1  17942  alexsublem  17998  ghmcnp  18067  divstgplem  18073  tsmssubm  18095  elutop  18186  ustuqtop4  18197  isucn  18231  iscfilu  18241  ismet  18264  isxmet  18265  ismet2  18274  imasdsf1olem  18313  blres  18353  elmopn  18364  mopni  18414  neibl  18423  nrmmetd  18495  ngppropd  18551  elcncf  18792  mulc1cncf  18808  elpi1  18943  metcld2  19132  pmltpclem1  19214  ovolval  19239  itg1climres  19475  itg2val  19489  isibl  19526  itgeq1f  19532  itgresr  19539  iblcn  19559  itgfsum  19587  dvreslem  19665  dvfsumlem2  19780  pf1ind  19844  deg1ldg  19884  vieta1  20098  ulm2  20170  sincosq2sgn  20276  sincosq4sgn  20278  efopn  20418  dvdsflsumcom  20842  fsumvma2  20867  logfac2  20870  dchrptlem1  20917  lgsdchrval  21000  pntibndlem3  21155  pntlemi  21167  pntleme  21171  pnt3  21175  usgra2edg  21270  trls  21402  istrl2  21404  trlon  21406  spths  21423  0spth  21427  pthon  21431  0crct  21463  0cycl  21464  usgrcyclnl2  21478  eupath2lem2  21550  drngoi  21845  rngosn3  21864  vci  21877  isvclem  21906  nmoofval  22113  isph  22173  norm3lemt  22504  isch2  22576  cmbr  22936  eigre  23188  eigorth  23191  nmopub  23261  nmfnleub  23278  cvbr  23635  mdbr  23647  dmdbr  23652  chrelat2  23723  mdsymlem2  23757  rexunirn  23824  ifeqeqx  23847  funcnvmptOLD  23925  funcnvmpt  23926  1stpreima  23938  gsumpropd2lem  24051  isofld  24063  ofldadd  24066  ofldmul  24067  dya2iocuni  24429  itgeq12dv  24437  isrrvv  24482  kur14  24683  pconcn  24692  cnpcon  24698  txpcon  24700  cvmscbv  24726  cvmcov  24731  cvmsi  24733  cvmsval  24734  cvmopnlem  24746  cvmlift2lem10  24780  cvmlift3lem2  24788  cvmlift3lem6  24792  cvmlift3lem7  24793  cvmlift3lem9  24795  cvmlift3  24796  relexp0  24910  relexpsucr  24911  relexpsucl  24913  relexpcnv  24914  relexpdm  24916  relexprn  24917  relexpadd  24919  relexpindlem  24920  rtrclreclem.trans  24927  rtrclreclem.min  24928  prodeq1f  25015  eldm3  25145  dfon2lem6  25170  dfon2lem7  25171  dfon2lem8  25172  dfon2  25174  preduz  25226  poseq  25279  soseq  25280  sltval  25327  nodenselem5  25365  nocvxminlem  25370  brimg  25502  brcgr  25555  brbtwn2  25560  axsegconlem1  25572  axsegcon  25582  axcontlem10  25628  brofs  25655  5segofs  25656  brifs  25693  ifscgr  25694  brcolinear  25709  lineext  25726  brfs  25729  fscgr  25730  linecgr  25731  btwnconn1lem4  25740  btwnconn1lem8  25744  btwnconn1lem11  25747  btwnconn1lem12  25748  segcon2  25755  brsegle  25758  outsideofeq  25780  funray  25790  funline  25792  fvline  25794  linethru  25803  itg2addnclem  25959  itg2addnc  25961  itg2gt0cn  25962  areacirclem6  25989  trer  26012  finminlem  26014  ivthALT  26031  locfinnei  26075  comppfsc  26080  filnetlem4  26103  cover2  26108  cover2g  26109  fdc  26142  fdc1  26143  heibor1  26212  bfp  26226  isdrngo1  26265  isriscg  26293  isfldidl2  26372  mrefg2  26454  mzpclval  26475  eldiophb  26508  eldioph2lem1  26511  eldioph3  26517  lzenom  26521  diophin  26524  eldiophss  26526  diophrex  26527  eq0rabdioph  26528  pellexlem3  26587  elpell1qr  26603  elpell14qr  26605  elpell1234qr  26607  jm2.27  26772  rmydioph  26778  expdiophlem1  26785  expdioph  26787  pw2f1ocnv  26801  islbs4  26973  islinds3  26975  hbtlem1  26998  hbtlem7  27000  dgraalem  27021  dgraaub  27024  psgnfval  27094  psgnval  27101  2sbc6g  27286  2sbc5g  27287  iotasbc  27290  dropab1  27320  dropab2  27321  dfdfat2  27666  3cyclfrgrarn1  27767  4cycl2vnunb  27772  bnj956  28487  bnj1146  28502  bnj18eq1  28638  drsb1NEW7  28846  islshpat  29134  lcvbr  29138  lshpsmreu  29226  ldual1dim  29283  cvrval  29386  cvrnbtwn3  29393  iscvlat2N  29441  ishlat3N  29471  hlrelat5N  29517  3dim0  29573  llnexatN  29637  islpln5  29651  islvol5  29695  pmapjat1  29969  ltrnu  30237  cdleme02N  30338  cdlemg33b  30823  cdlemg33c  30824  dvhb1dimN  31102  dibelval3  31264  dibopelval3  31265  dib1dim  31282  dibglbN  31283  diblsmopel  31288  dicval  31293  dicopelval  31294  dicelval3  31297  dicelval1sta  31304  dihopelvalcpre  31365  dih1dimatlem  31446  dihpN  31453  dihjatcclem4  31538  lpolsetN  31599  mapdpglem3  31792  hdmapglem7a  32047
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator