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

Theorem anbi1d 685
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 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 621 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi1  687  anbi12d  691  bi2anan9  843  pm5.71  902  cador  1396  drsb1  2035  eleq1  2426  rexeqf  2818  reueq1f  2819  rmoeq1f  2820  rabeqf  2866  vtocl2gaf  2935  alexeq  2982  ceqex  2983  elrabi  3007  sbc2or  3085  sbc5  3101  rexss  3326  psstr  3367  ineq1  3451  difin2  3518  r19.28z  3635  r19.28zv  3638  ssunsn2  3873  preq12bg  3891  opeq1  3898  eluni  3932  disjxun  4123  mpteq12f  4198  axrep1  4234  axrep2  4235  axrep3  4236  zfrepclf  4239  axsep  4242  axsep2  4244  zfauscl  4245  opthg  4349  copsexg  4355  euotd  4370  elopab  4375  pocl  4424  dflim2  4551  uniuni  4630  reusv2lem4  4641  rabxfrd  4658  limuni3  4746  xpeq1  4806  elxpi  4808  vtoclr  4836  opbrop  4870  opelresg  5065  resopab2  5102  elxp4  5263  elxp5  5264  fun11  5420  feq2  5481  f1eq2  5539  f1eq3  5540  foeq2  5554  brprcneu  5625  ssimaexg  5692  dmfco  5700  fndmdif  5736  rexsupp  5757  respreima  5761  opabex3d  5889  opabex3  5890  isoeq5  5943  isoini  5958  isopolem  5965  f1oiso  5971  f1oiso2  5972  oprabid  6005  mpt2eq123  6033  mpt2eq123dva  6035  eloprabga  6060  resoprab  6066  resoprab2  6067  ov  6093  ov3  6110  ov6g  6111  ovg  6112  caoftrn  6239  eloprabi  6313  cnvf1o  6345  frxp  6353  xporderlem  6354  poxp  6355  fnwelem  6358  opiota  6432  riotaeqdv  6447  smoel2  6522  omeu  6725  oeeui  6742  omabs  6787  omopth  6798  qliftel  6884  brecop  6894  eroveu  6896  erov  6898  ecopovtrn  6904  th3qlem2  6908  th3q  6910  ixpsnf1o  6999  dom2lem  7044  xpsnen  7089  xpassen  7099  pw2f1olem  7109  xpf1o  7166  unxpdom  7213  domunfican  7276  preleq  7465  zfinf  7487  cantnfs  7514  tcvalg  7570  r0weon  7787  fseqenlem1  7798  acni2  7820  aceq1  7891  aceq0  7892  dfac2a  7903  dfac12lem2  7917  cardcf  8025  cfeq0  8029  cfsuc  8030  cff1  8031  cfss  8038  isf32lem5  8130  fin1a2lem6  8178  zfac  8233  brdom7disj  8303  brdom6disj  8304  axrepnd  8363  axunndlem1  8364  axinfnd  8375  axacndlem5  8380  axacnd  8381  zfcndrep  8383  zfcndinf  8387  zfcndac  8388  pwfseqlem4a  8430  pwfseqlem4  8431  gruina  8587  grothomex  8598  ordpipq  8713  elnpi  8759  genpass  8780  ltprord  8801  reclem2pr  8819  reclem3pr  8820  recexpr  8822  ltsosr  8863  mulgt0sr  8874  supsr  8881  ltresr  8909  axpre-lttrn  8935  axpre-mulgt0  8937  prime  10243  peano5uzti  10252  uzindOLD  10257  rexuz  10420  ltxr  10608  qbtwnre  10678  xmulneg1  10741  supxr2  10785  ixxval  10817  fzval  10937  nn0opth2  11452  hashbclem  11588  hashf1lem2  11592  abslt  12005  absle  12006  lenegsq  12011  abs2difabs  12025  ello12  12197  elo12  12208  o1lo1  12218  rlimuni  12231  lo1resb  12245  o1resb  12247  2clim  12253  rlimcn2  12271  climcn2  12273  addcn2  12274  mulcn2  12276  o1of2  12293  sumeq1f  12369  fsum2dlem  12441  znnenlem  12698  nndivdvds  12745  divalg2  12812  smupval  12887  gcdval  12895  gcdass  12932  rpexp  13007  pythagtriplem2  13078  pythagtrip  13095  vdwapun  13229  0ram  13275  ramub1lem2  13282  pwsle  13601  imasleval  13653  ismre  13702  ismri  13743  iscatd2  13793  isssc  13907  funcpropd  13984  fullpropd  14004  fthres2b  14014  fthres2c  14015  setcsect  14131  prslem  14275  drsdir  14279  posi  14294  tosso  14352  ipoval  14467  ipolt  14472  odudlatb  14509  dirge  14569  mndpropd  14608  mhmpropd  14631  issubg3  14847  isga  14955  isslw  15129  dprdw  15455  subgdmdprd  15479  drngpropd  15749  issubrg  15755  islmod  15841  lmodlema  15842  lmodprop2d  15897  lsslss  15928  lbspropd  16062  lbsacsbs  16119  aspval2  16296  psrbag  16322  znleval  16725  istopg  16858  basis2  16906  tg2  16920  iscld  16981  neival  17056  isnei  17057  isneip  17059  restlp  17130  iscn  17182  cnpval  17183  iscnp  17184  regsep  17279  nrmsep3  17300  1stcclb  17387  2ndc1stc  17394  2ndcctbss  17398  2ndcdisj  17399  llyi  17417  nllyi  17418  hausmapdom  17443  elkgen  17448  txbas  17479  txcls  17516  txcnpi  17519  ptpjopn  17523  txdis1cn  17546  txtube  17551  txcmplem1  17552  hausdiag  17556  tx1stc  17561  txkgen  17563  xkococnlem  17570  xkococn  17571  elqtop  17605  kqreglem1  17649  elmptrab  17735  isfbas  17737  elflim2  17872  elflim  17879  hauspwpwf1  17895  alexsublem  17951  ghmcnp  18010  divstgplem  18016  tsmssubm  18038  ismet  18101  isxmet  18102  ismet2  18111  imasdsf1olem  18150  blres  18190  elmopn  18201  mopni  18251  neibl  18260  nrmmetd  18310  ngppropd  18366  elcncf  18607  mulc1cncf  18623  elpi1  18758  metcld2  18947  pmltpclem1  19023  ovolval  19048  itg1climres  19284  itg2val  19298  isibl  19335  itgeq1f  19341  itgresr  19348  iblcn  19368  itgfsum  19396  dvreslem  19474  dvfsumlem2  19589  pf1ind  19653  deg1ldg  19693  vieta1  19907  ulm2  19979  sincosq2sgn  20085  sincosq4sgn  20087  efopn  20227  dvdsflsumcom  20651  fsumvma2  20676  logfac2  20679  dchrptlem1  20726  lgsdchrval  20809  pntibndlem3  20964  pntlemi  20976  pntleme  20980  pnt3  20984  usgra2edg  21079  eupath2lem2  21211  drngoi  21506  rngosn3  21525  vci  21538  isvclem  21567  nmoofval  21774  isph  21834  norm3lemt  22165  isch2  22237  cmbr  22597  eigre  22849  eigorth  22852  nmopub  22922  nmfnleub  22939  cvbr  23296  mdbr  23308  dmdbr  23313  chrelat2  23384  mdsymlem2  23418  rexunirn  23493  ifeqeqx  23520  funcnvmptOLD  23605  funcnvmpt  23606  1stpreima  23619  gsumpropd2lem  23732  neiptoptop  23764  neiptopnei  23765  elutop  23857  ustuqtop4  23868  isucn  23894  iscfilu  23902  dya2iocuni  24217  itgeq12dv  24225  isrrvv  24270  kur14  24471  pconcn  24479  cnpcon  24485  txpcon  24487  cvmscbv  24513  cvmcov  24518  cvmsi  24520  cvmsval  24521  cvmopnlem  24533  cvmlift2lem10  24567  cvmlift3lem2  24575  cvmlift3lem6  24579  cvmlift3lem7  24580  cvmlift3lem9  24582  cvmlift3  24583  relexp0  24697  relexpsucr  24698  relexpsucl  24700  relexpcnv  24701  relexpdm  24704  relexprn  24705  relexpadd  24707  relexpindlem  24708  rtrclreclem.trans  24715  rtrclreclem.min  24716  prodeq1f  24803  eldm3  24945  dfon2lem6  24970  dfon2lem7  24971  dfon2lem8  24972  dfon2  24974  preduz  25026  poseq  25079  soseq  25080  sltval  25127  nodenselem5  25165  nocvxminlem  25170  brimg  25302  brcgr  25355  brbtwn2  25360  axsegconlem1  25372  axsegcon  25382  axcontlem10  25428  brofs  25455  5segofs  25456  brifs  25493  ifscgr  25494  brcolinear  25509  lineext  25526  brfs  25529  fscgr  25530  linecgr  25531  btwnconn1lem4  25540  btwnconn1lem8  25544  btwnconn1lem11  25547  btwnconn1lem12  25548  segcon2  25555  brsegle  25558  outsideofeq  25580  funray  25590  funline  25592  fvline  25594  linethru  25603  itg2addnclem  25760  itg2addnc  25762  itg2gt0cn  25763  areacirclem6  25790  trer  25819  finminlem  25823  ivthALT  25850  locfinnei  25894  comppfsc  25899  filnetlem4  25922  cover2  25950  cover2g  25951  fdc  26047  fdc1  26048  heibor1  26125  bfp  26139  isdrngo1  26178  isriscg  26206  isfldidl2  26285  mrefg2  26373  mzpclval  26394  eldiophb  26427  eldioph2lem1  26430  eldioph3  26436  lzenom  26440  diophin  26443  eldiophss  26445  diophrex  26446  eq0rabdioph  26447  pellexlem3  26507  elpell1qr  26523  elpell14qr  26525  elpell1234qr  26527  jm2.27  26692  rmydioph  26698  expdiophlem1  26705  expdioph  26707  pw2f1ocnv  26721  islbs4  26893  islinds3  26895  hbtlem1  26918  hbtlem7  26920  dgraalem  26941  dgraaub  26944  psgnfval  27014  psgnval  27021  2sbc6g  27206  2sbc5g  27207  iotasbc  27210  dropab1  27241  dropab2  27242  stoweidlem57  27397  dfdfat2  27587  trls  27699  istrl2  27701  trlon  27703  spths  27720  0spth  27724  pthon  27728  0crct  27760  0cycl  27761  usgrcyclnl2  27776  3cyclfrgrarn1  27836  4cycl2vnunb  27841  bnj956  28560  bnj1146  28575  bnj18eq1  28711  drsb1NEW7  28919  islshpat  29266  lcvbr  29270  lshpsmreu  29358  ldual1dim  29415  cvrval  29518  cvrnbtwn3  29525  iscvlat2N  29573  ishlat3N  29603  hlrelat5N  29649  3dim0  29705  llnexatN  29769  islpln5  29783  islvol5  29827  pmapjat1  30101  ltrnu  30369  cdleme02N  30470  cdlemg33b  30955  cdlemg33c  30956  dvhb1dimN  31234  dibelval3  31396  dibopelval3  31397  dib1dim  31414  dibglbN  31415  diblsmopel  31420  dicval  31425  dicopelval  31426  dicelval3  31429  dicelval1sta  31436  dihopelvalcpre  31497  dih1dimatlem  31578  dihpN  31585  dihjatcclem4  31670  lpolsetN  31731  mapdpglem3  31924  hdmapglem7a  32179
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 177  df-an 360
  Copyright terms: Public domain W3C validator