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

Theorem anbi1d 704
Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-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 25 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 640 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  anbi1  706  anbi12d  710  bi2anan9  868  pm5.71  927  cador  1432  drsb1  2068  eleq1  2503  rexeqf  2935  reueq1f  2936  rmoeq1f  2937  rabeqf  2986  vtocl2gaf  3058  vtocl4ga  3063  alexeqg  3109  alexeq  3110  elrabi  3135  sbc2or  3216  sbc5  3232  rexss  3440  psstr  3481  ineq1  3566  difin2  3633  r19.28z  3793  r19.28zv  3796  rabsnifsb  3964  ssunsn2  4053  preq12bg  4072  prel12g  4073  opeq1  4080  eluni  4115  csbuni  4140  disjxun  4311  mpteq12f  4389  axrep1  4425  axrep2  4426  axrep3  4427  zfrepclf  4430  axsep  4433  axsep2  4435  zfauscl  4436  reusv2lem4  4517  rabxfrd  4534  opthg  4588  copsexg  4597  copsexgOLD  4598  euotd  4613  elopab  4618  pocl  4669  dflim2  4796  xpeq1  4875  elxpi  4877  vtoclr  4904  opbrop  4937  opelresg  5139  resopab2  5176  fun11  5504  feq2  5564  f1eq2  5623  f1eq3  5624  foeq2  5638  brprcneu  5705  ssimaexg  5778  dmfco  5786  fndmdif  5828  rexsuppOLD  5849  respreima  5853  isoeq5  6035  isoini  6050  isopolem  6057  f1oiso  6063  f1oiso2  6064  riotaeqdv  6074  oprabid  6136  mpt2eq123  6166  mpt2eq123dva  6168  eloprabga  6198  resoprab  6207  resoprab2  6208  elrnmpt2res  6225  ov  6231  ov3  6248  ov6g  6249  ovg  6250  caoftrn  6376  uniuni  6406  limuni3  6484  elxp4  6543  elxp5  6544  opabex3d  6576  opabex3  6577  opiota  6654  eloprabi  6657  cnvf1o  6692  frxp  6703  xporderlem  6704  poxp  6705  fnwelem  6708  suppimacnv  6722  rexsupp  6728  mpt2curryd  6809  smoel2  6845  omeu  7045  oeeui  7062  omabs  7107  omopth  7118  qliftel  7204  brecop  7214  eroveu  7216  erov  7218  ecopovtrn  7224  th3qlem2  7228  th3q  7230  ixpsnf1o  7324  dom2lem  7370  xpsnen  7416  xpassen  7426  pw2f1olem  7436  xpf1o  7494  unxpdom  7541  domunfican  7605  preleq  7844  zfinf  7866  cantnfs  7895  cantnfsOLD  7925  tcvalg  7979  r0weon  8200  fseqenlem1  8215  acni2  8237  aceq1  8308  aceq0  8309  dfac2a  8320  dfac12lem2  8334  cardcf  8442  cfeq0  8446  cfsuc  8447  cff1  8448  cfss  8455  isf32lem5  8547  fin1a2lem6  8595  zfac  8650  brdom7disj  8719  brdom6disj  8720  axrepnd  8779  axunndlem1  8780  axinfnd  8794  axacndlem5  8799  axacnd  8800  zfcndrep  8802  zfcndinf  8806  zfcndac  8807  pwfseqlem4a  8849  pwfseqlem4  8850  gruina  9006  grothomex  9017  ordpipq  9132  elnpi  9178  genpass  9199  ltprord  9220  reclem2pr  9238  reclem3pr  9239  recexpr  9241  ltsosr  9282  mulgt0sr  9293  supsr  9300  ltresr  9328  axpre-lttrn  9354  axpre-mulgt0  9356  prime  10743  peano5uzti  10752  uzindOLD  10757  rexuz  10926  ltxr  11116  qbtwnre  11190  xmulneg1  11253  supxr2  11297  ixxval  11329  fzval  11460  nn0opth2  12071  hashbclem  12226  hashf1lem2  12230  eqwrd  12286  swrdeq  12361  wrd2ind  12393  abslt  12823  absle  12824  lenegsq  12829  abs2difabs  12843  ello12  13015  elo12  13026  o1lo1  13036  rlimuni  13049  lo1resb  13063  o1resb  13065  2clim  13071  rlimcn2  13089  climcn2  13091  addcn2  13092  mulcn2  13094  o1of2  13111  sumeq1  13187  fsum2dlem  13258  znnenlem  13515  nndivdvds  13562  divalg2  13630  smupval  13705  gcdval  13713  gcdass  13750  rpexp  13827  pythagtriplem2  13905  pythagtrip  13922  vdwapun  14056  0ram  14102  ramub1lem2  14109  pwsle  14451  imasleval  14500  ismre  14549  ismri  14590  iscatd2  14640  isssc  14754  funcpropd  14831  fullpropd  14851  fthres2b  14861  fthres2c  14862  setcsect  14978  prslem  15122  drsdir  15126  posi  15141  tosso  15227  ipoval  15345  ipolt  15350  odudlatb  15387  dirge  15428  mndpropd  15467  mhmpropd  15491  mrcmndind  15515  gsumpropd2lem  15526  issubg3  15720  isga  15830  symgfixelq  15959  psgnfval  16027  psgnval  16034  isslw  16128  dprdw  16516  dprdwOLD  16522  subgdmdprd  16553  drngpropd  16881  issubrg  16887  islmod  16974  lmodlema  16975  lmodprop2d  17029  lsslss  17064  lbspropd  17202  lbsacsbs  17259  aspval2  17439  psrbag  17453  pf1ind  17811  znleval  18009  islbs4  18283  islinds3  18285  mdetunilem4  18443  mdetunilem9  18448  istopg  18530  basis2  18578  tg2  18592  iscld  18653  neival  18728  isnei  18729  isneip  18731  neiptoptop  18757  neiptopnei  18758  neitr  18806  restlp  18809  iscn  18861  cnpval  18862  iscnp  18863  regsep  18960  nrmsep3  18981  1stcclb  19070  2ndc1stc  19077  2ndcctbss  19081  2ndcdisj  19082  llyi  19100  nllyi  19101  hausmapdom  19126  elkgen  19131  txbas  19162  txcls  19199  txcnpi  19203  ptpjopn  19207  txdis1cn  19230  txtube  19235  txcmplem1  19236  hausdiag  19240  tx1stc  19245  txkgen  19247  xkococnlem  19254  xkococn  19255  elqtop  19292  kqreglem1  19336  elmptrab  19422  isfbas  19424  elflim2  19559  elflim  19566  hauspwpwf1  19582  alexsublem  19638  ghmcnp  19707  divstgplem  19713  tsmssubm  19738  elutop  19830  ustuqtop4  19841  isucn  19875  iscfilu  19885  ispsmet  19902  ismet  19920  isxmet  19921  ismet2  19930  imasdsf1olem  19970  blres  20028  elmopn  20039  mopni  20089  neibl  20098  nrmmetd  20189  ngppropd  20245  elcncf  20487  mulc1cncf  20503  elpi1  20639  metcld2  20839  pmltpclem1  20954  ovolval  20979  itg1climres  21214  itg2val  21228  isibl  21265  itgeq1f  21271  itgresr  21278  iblcn  21298  itgfsum  21326  dvreslem  21406  dvfsumlem2  21521  deg1ldg  21585  vieta1  21800  ulm2  21872  sincosq2sgn  21983  sincosq4sgn  21985  efopn  22125  dvdsflsumcom  22550  fsumvma2  22575  logfac2  22578  dchrptlem1  22625  lgsdchrval  22708  pntibndlem3  22863  pntlemi  22875  pntleme  22879  pnt3  22883  istrkg2d  22944  axtgsegcon  22947  axtg5seg  22948  axtgpasch  22950  axtgupdim2  22954  legov  23038  brcgr  23168  brbtwn2  23173  axsegconlem1  23185  axsegcon  23195  axcontlem10  23241  usgra2edg  23323  trls  23457  istrl2  23459  trlon  23461  is2wlk  23486  spths  23488  0spth  23492  pthon  23496  spthon  23503  isspthonpth  23505  0crct  23534  0cycl  23535  usgrcyclnl2  23549  eupath2lem2  23621  drngoi  23916  rngosn3  23935  vci  23948  isvclem  23977  nmoofval  24184  isph  24244  norm3lemt  24576  isch2  24648  cmbr  25009  eigre  25261  eigorth  25264  nmopub  25334  nmfnleub  25351  cvbr  25708  mdbr  25720  dmdbr  25725  chrelat2  25796  mdsymlem2  25830  rexunirn  25897  ifeqeqx  25924  funcnvmptOLD  26008  funcnvmpt  26009  1stpreima  26023  fpwrelmapffslem  26054  isomnd  26186  archirng  26227  isslmd  26240  slmdlema  26241  dya2iocuni  26720  omsfval  26731  itgeq12dv  26734  isrrvv  26848  brafs  27018  kur14  27126  pconcn  27135  cnpcon  27141  txpcon  27143  cvmscbv  27169  cvmcov  27174  cvmsi  27176  cvmsval  27177  cvmopnlem  27189  cvmlift2lem10  27223  cvmlift3lem2  27231  cvmlift3lem6  27235  cvmlift3lem7  27236  cvmlift3lem9  27238  cvmlift3  27239  relexp0  27353  relexpsucr  27354  relexpsucl  27356  relexpcnv  27357  relexpdm  27359  relexprn  27360  relexpadd  27362  relexpindlem  27363  rtrclreclem.trans  27370  rtrclreclem.min  27371  prodeq1f  27443  fprod2dlem  27513  eldm3  27594  opelco3  27611  dfon2lem6  27623  dfon2lem7  27624  dfon2lem8  27625  dfon2  27627  preduz  27683  poseq  27736  soseq  27737  sltval  27810  nodenselem5  27848  nocvxminlem  27853  elfuns  27968  brofs  28058  5segofs  28059  brifs  28096  ifscgr  28097  brcolinear  28112  lineext  28129  brfs  28132  fscgr  28133  linecgr  28134  btwnconn1lem4  28143  btwnconn1lem8  28147  btwnconn1lem11  28150  btwnconn1lem12  28151  segcon2  28158  brsegle  28161  outsideofeq  28183  funray  28193  funline  28195  fvline  28197  linethru  28206  wl-ax11-lem8  28434  ptrest  28451  heicant  28452  mblfinlem3  28456  mblfinlem4  28457  mbfresfi  28464  itg2addnclem3  28471  itg2addnc  28472  itg2gt0cn  28473  areacirclem5  28514  trer  28537  finminlem  28539  ivthALT  28556  locfinnei  28600  comppfsc  28605  filnetlem4  28628  cover2  28633  cover2g  28634  fdc  28667  fdc1  28668  heibor1  28735  bfp  28749  isdrngo1  28788  isriscg  28816  isfldidl2  28895  mrefg2  29069  mzpclval  29087  eldiophb  29121  eldioph2lem1  29124  eldioph3  29130  lzenom  29134  diophin  29137  eldiophss  29139  diophrex  29140  eq0rabdioph  29141  pellexlem3  29198  elpell1qr  29214  elpell14qr  29216  elpell1234qr  29218  jm2.27  29383  rmydioph  29389  expdiophlem1  29396  expdioph  29398  pw2f1ocnv  29412  hbtlem1  29505  hbtlem7  29507  dgraalem  29528  dgraaub  29531  2sbc6g  29695  2sbc5g  29696  iotasbc  29699  dropab1  29729  dropab2  29730  dfdfat2  30063  otthg  30156  oprabv  30183  2ffzoeq  30240  modfsummod  30271  usgra2wlkspthlem1  30322  spthdifv  30325  usgra2pth  30327  wwlknprop  30346  vfwlkniswwlkn  30366  wwlknext  30382  wwlknfi  30396  el2wlkonotot0  30417  2spontn0vne  30432  clwlk  30444  isclwlk  30447  clwlkcompim  30453  clwwlkn2  30464  clwwlknimp  30465  clwwlkel  30481  clwwlkf  30482  clwwlkext2edg  30490  wwlkext2clwwlk  30491  wwlksubclwwlk  30492  erclwwlktr0  30505  erclwwlknsym  30526  erclwwlkntr  30527  clwlkfoclwwlk  30544  rusgranumwlkl1  30585  rusgranumwlklem3  30595  rusgranumwlkb0  30597  rusgra0edg  30599  3cyclfrgrarn1  30630  4cycl2vnunb  30635  frg2wot1  30676  usg2spot2nb  30684  extwwlkfablem2  30697  numclwwlkovfel2  30702  numclwwlkovf2  30703  numclwwlkovf2ex  30705  numclwwlkovgel  30707  numclwwlkovgelim  30708  numclwlk2lem2f  30722  numclwlk2lem2f1o  30724  numclwwlk5  30731  lmod1  31031  bnj956  31866  bnj1146  31881  bnj18eq1  32016  bj-axrep1  32405  bj-axrep2  32406  bj-axrep3  32407  bj-axsep  32410  bj-eleq1w  32453  bj-rabeqd  32519  bj-axsep2  32524  islshpat  32758  lcvbr  32762  lshpsmreu  32850  ldual1dim  32907  cvrval  33010  cvrnbtwn3  33017  iscvlat2N  33065  ishlat3N  33095  hlrelat5N  33141  3dim0  33197  llnexatN  33261  islpln5  33275  islvol5  33319  pmapjat1  33593  ltrnu  33861  cdleme02N  33962  cdlemg33b  34447  cdlemg33c  34448  dvhb1dimN  34726  dibelval3  34888  dibopelval3  34889  dib1dim  34906  dibglbN  34907  diblsmopel  34912  dicval  34917  dicopelval  34918  dicelval3  34921  dicelval1sta  34928  dihopelvalcpre  34989  dih1dimatlem  35070  dihpN  35077  dihjatcclem4  35162  lpolsetN  35223  mapdpglem3  35416  hdmapglem7a  35671
  Copyright terms: Public domain W3C validator