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

Theorem anbi1d 702
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 638 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  anbi1  704  anbi12d  708  bi2anan9  871  pm5.71  934  cador  1465  drsb1  2122  eleq1d  2451  eleq1OLD  2456  rexeqf  2976  reueq1f  2977  rmoeq1f  2978  rabeqf  3027  vtocl2gaf  3099  vtocl4ga  3104  alexeqg  3153  alexeq  3154  elrabi  3179  reu2eqd  3221  sbc2or  3261  sbc5  3277  rexss  3481  psstr  3522  ineq1  3607  difin2  3685  r19.28z  3837  r19.28zv  3840  rabsnifsb  4012  ssunsn2  4103  preq12bg  4123  prel12g  4124  opeq1  4131  eluni  4166  csbuni  4191  disjxun  4365  mpteq12f  4443  axrep1  4479  axrep2  4480  axrep3  4481  zfrepclf  4484  axsep  4487  axsep2  4489  zfauscl  4490  reusv2lem4  4569  rabxfrd  4583  opthg  4637  otthg  4645  copsexg  4647  euotd  4662  elopab  4669  pocl  4721  dflim2  4848  xpeq1  4927  elxpi  4929  vtoclr  4958  opbrop  4993  opelresg  5193  resopab2  5234  fun11  5561  feq2  5622  f1eq2  5685  f1eq3  5686  foeq2  5700  brprcneu  5767  ssimaexg  5840  dmfco  5848  fndmdif  5893  rexsuppOLD  5914  respreima  5918  isoeq5  6120  isoini  6135  isopolem  6142  f1oiso  6148  f1oiso2  6149  riotaeqdv  6159  oprabid  6223  oprabv  6244  mpt2eq123  6255  mpt2eq123dva  6257  eloprabga  6288  resoprab  6297  resoprab2  6298  elrnmpt2res  6315  ov  6321  ov3  6338  ov6g  6339  ovg  6340  caoftrn  6474  uniuni  6508  limuni3  6586  elxp4  6643  elxp5  6644  opabex3d  6677  opabex3  6678  opiota  6758  eloprabi  6761  cnvf1o  6798  frxp  6809  xporderlem  6810  poxp  6811  fnwelem  6814  suppimacnv  6828  rexsupp  6836  mpt2curryd  6916  smoel2  6952  omeu  7152  oeeui  7169  omabs  7214  omopth  7225  qliftel  7312  brecop  7322  eroveu  7324  erov  7326  ecopovtrn  7332  ixpsnf1o  7428  dom2lem  7474  xpsnen  7520  xpassen  7530  pw2f1olem  7540  xpf1o  7598  unxpdom  7643  domunfican  7708  preleq  7948  zfinf  7970  cantnfs  7998  cantnfsOLD  8028  tcvalg  8082  r0weon  8303  fseqenlem1  8318  acni2  8340  aceq1  8411  aceq0  8412  dfac2a  8423  dfac12lem2  8437  cardcf  8545  cfeq0  8549  cfsuc  8550  cff1  8551  cfss  8558  isf32lem5  8650  fin1a2lem6  8698  zfac  8753  brdom7disj  8822  brdom6disj  8823  axrepnd  8882  axunndlem1  8883  axinfnd  8895  axacndlem5  8900  axacnd  8901  zfcndrep  8903  zfcndinf  8907  zfcndac  8908  pwfseqlem4a  8950  pwfseqlem4  8951  gruina  9107  grothomex  9118  ordpipq  9231  elnpi  9277  genpass  9298  ltprord  9319  reclem2pr  9337  reclem3pr  9338  recexpr  9340  addsrmo  9361  mulsrmo  9362  addsrpr  9363  mulsrpr  9364  ltsosr  9382  mulgt0sr  9393  supsr  9400  ltresr  9428  axpre-lttrn  9454  axpre-mulgt0  9456  prime  10860  peano5uzti  10869  rexuz  11051  ltxr  11245  qbtwnre  11319  xmulneg1  11382  supxr2  11426  ixxval  11458  fzval  11595  nn0opth2  12254  hashbclem  12405  hashf1lem2  12409  eqwrd  12490  swrdeq  12580  wrd2ind  12614  cshwcsh2id  12707  cleq1lem  12820  rtrclreclem3  12895  rtrclreclem4  12896  relexpindlem  12898  abslt  13149  absle  13150  lenegsq  13155  abs2difabs  13169  ello12  13341  elo12  13352  o1lo1  13362  rlimuni  13375  lo1resb  13389  o1resb  13391  2clim  13397  rlimcn2  13415  climcn2  13417  addcn2  13418  mulcn2  13420  o1of2  13437  sumeq1  13513  fsum2dlem  13587  modfsummod  13610  prodeq1f  13717  fprod2dlem  13786  znnenlem  13947  nndivdvds  13994  divalg2  14065  smupval  14140  gcdval  14148  gcdass  14185  rpexp  14263  pythagtriplem2  14343  pythagtrip  14360  vdwapun  14494  0ram  14540  ramub1lem2  14547  pwsle  14899  imasleval  14948  ismre  14997  ismri  15038  iscatd2  15088  dfiso2  15178  isssc  15226  funcpropd  15306  fullpropd  15326  fthres2b  15336  fthres2c  15337  setcsect  15485  prslem  15677  drsdir  15681  posi  15696  tosso  15783  ipoval  15901  ipolt  15906  odudlatb  15943  dirge  15984  gsumpropd2lem  16017  issgrpv  16030  issgrpn0  16031  mhmpropd  16089  mrcmndind  16114  mgmnsgrpex  16166  issubg3  16336  isga  16446  symgfixelq  16575  psgnfval  16642  psgnval  16649  isslw  16745  dprdw  17156  dprdwOLD  17163  subgdmdprd  17194  drngpropd  17536  issubrg  17542  islmod  17629  lmodlema  17630  lmodprop2d  17685  lsslss  17720  lbspropd  17858  lbsacsbs  17915  aspval2  18109  psrbag  18126  pf1ind  18504  znleval  18684  islbs4  18952  islinds3  18954  mdetunilem4  19202  mdetunilem9  19207  istopg  19489  basis2  19537  tg2  19551  iscld  19613  neival  19689  isnei  19690  isneip  19692  neiptoptop  19718  neiptopnei  19719  neitr  19767  restlp  19770  iscn  19822  cnpval  19823  iscnp  19824  regsep  19921  nrmsep3  19942  1stcclb  20030  2ndc1stc  20037  2ndcctbss  20041  2ndcdisj  20042  llyi  20060  nllyi  20061  hausmapdom  20086  locfinnei  20109  comppfsc  20118  elkgen  20122  txbas  20153  txcls  20190  txcnpi  20194  ptpjopn  20198  txdis1cn  20221  txtube  20226  txcmplem1  20227  hausdiag  20231  tx1stc  20236  txkgen  20238  xkococnlem  20245  xkococn  20246  elqtop  20283  kqreglem1  20327  elmptrab  20413  isfbas  20415  elflim2  20550  elflim  20557  hauspwpwf1  20573  alexsublem  20629  ghmcnp  20698  qustgplem  20704  tsmssubm  20729  elutop  20821  ustuqtop4  20832  isucn  20866  iscfilu  20876  ispsmet  20893  ismet  20911  isxmet  20912  ismet2  20921  imasdsf1olem  20961  blres  21019  elmopn  21030  mopni  21080  neibl  21089  nrmmetd  21180  ngppropd  21236  elcncf  21478  mulc1cncf  21494  elpi1  21630  metcld2  21830  pmltpclem1  21945  ovolval  21970  itg1climres  22206  itg2val  22220  isibl  22257  itgeq1f  22263  itgresr  22270  iblcn  22290  itgfsum  22318  dvreslem  22398  dvfsumlem2  22513  deg1ldg  22577  vieta1  22793  ulm2  22865  sincosq2sgn  22977  sincosq4sgn  22979  efopn  23126  dvdsflsumcom  23581  fsumvma2  23606  logfac2  23609  dchrptlem1  23656  lgsdchrval  23739  pntibndlem3  23894  pntlemi  23906  pntleme  23910  pnt3  23914  istrkg2d  23973  istrkgld  23974  istrkg2ld  23975  axtgsegcon  23978  axtg5seg  23979  axtgpasch  23981  axtgupdim2  23986  legov  24092  islnopp  24233  ishpg  24248  brcgr  24324  brbtwn2  24329  axsegconlem1  24341  axsegcon  24351  axcontlem10  24397  usgra2edg  24503  trls  24659  istrl2  24661  trlon  24663  is2wlk  24688  spths  24690  0spth  24694  pthon  24698  spthon  24705  isspthonpth  24707  usgra2wlkspthlem1  24740  0crct  24747  0cycl  24748  usgrcyclnl2  24762  wwlknprop  24807  vfwlkniswwlkn  24827  wwlknext  24845  wwlknfi  24859  clwlk  24874  isclwlk  24877  clwlkcompim  24885  clwwlkn2  24896  clwwlknimp  24897  clwwlkel  24914  clwwlkf  24915  clwwlkext2edg  24923  wwlkext2clwwlk  24924  wwlksubclwwlk  24925  erclwwlknsym  24947  erclwwlkntr  24948  clwlkfoclwwlk  24966  el2wlkonotot0  24993  2spontn0vne  25008  rusgranumwlkl1  25068  rusgranumwlklem3  25072  rusgranumwlkb0  25074  rusgra0edg  25076  eupath2lem2  25099  3cyclfrgrarn1  25133  4cycl2vnunb  25138  frg2wot1  25178  usg2spot2nb  25186  extwwlkfablem2  25199  numclwwlkovfel2  25204  numclwwlkovf2  25205  numclwwlkovf2ex  25207  numclwwlkovgel  25209  numclwwlkovgelim  25210  numclwlk2lem2f  25224  numclwlk2lem2f1o  25226  numclwwlk5  25233  drngoi  25526  rngosn3  25545  vci  25558  isvclem  25587  nmoofval  25794  isph  25854  norm3lemt  26186  isch2  26258  cmbr  26619  eigre  26870  eigorth  26873  nmopub  26943  nmfnleub  26960  cvbr  27317  mdbr  27329  dmdbr  27334  chrelat2  27405  mdsymlem2  27439  rexunirn  27507  ifeqeqx  27544  funcnvmptOLD  27655  funcnvmpt  27656  1stpreima  27672  fpwrelmapffslem  27705  isomnd  27844  archirng  27885  isslmd  27898  slmdlema  27899  orngmul  27947  dya2iocuni  28410  omsfval  28421  elcarsg  28432  itgeq12dv  28451  isrrvv  28565  brafs  28735  kur14  28849  pconcn  28858  cnpcon  28864  txpcon  28866  cvmscbv  28892  cvmcov  28897  cvmsi  28899  cvmsval  28900  cvmopnlem  28912  cvmlift2lem10  28946  cvmlift3lem2  28954  cvmlift3lem6  28958  cvmlift3lem7  28959  cvmlift3lem9  28961  cvmlift3  28962  mclsssvlem  29111  mclsind  29119  eldm3  29357  opelco3  29373  dfon2lem6  29385  dfon2lem7  29386  dfon2lem8  29387  dfon2  29389  preduz  29445  poseq  29498  soseq  29499  sltval  29572  nodenselem5  29610  nocvxminlem  29615  elfuns  29718  brofs  29808  5segofs  29809  brifs  29846  ifscgr  29847  brcolinear  29862  lineext  29879  brfs  29882  fscgr  29883  linecgr  29884  btwnconn1lem4  29893  btwnconn1lem8  29897  btwnconn1lem11  29900  btwnconn1lem12  29901  segcon2  29908  brsegle  29911  outsideofeq  29933  funray  29943  funline  29945  fvline  29947  linethru  29956  wl-ax11-lem8  30197  ptrest  30213  heicant  30214  mblfinlem3  30218  mblfinlem4  30219  mbfresfi  30226  itg2addnclem3  30234  itg2addnc  30235  itg2gt0cn  30236  areacirclem5  30277  trer  30300  finminlem  30302  ivthALT  30319  filnetlem4  30365  cover2  30370  cover2g  30371  fdc  30404  fdc1  30405  heibor1  30472  bfp  30486  isdrngo1  30525  isriscg  30553  isfldidl2  30632  mrefg2  30805  mzpclval  30823  eldiophb  30855  eldioph2lem1  30858  eldioph3  30864  lzenom  30868  diophin  30871  eldiophss  30873  diophrex  30874  eq0rabdioph  30875  pellexlem3  30932  elpell1qr  30948  elpell14qr  30950  elpell1234qr  30952  jm2.27  31116  rmydioph  31122  expdiophlem1  31129  expdioph  31131  pw2f1ocnv  31145  hbtlem1  31240  hbtlem7  31242  dgraalem  31262  dgraaub  31265  lcmval  31366  lcmass  31386  binomcxplemnotnn0  31429  2sbc6g  31490  2sbc5g  31491  iotasbc  31494  dropab1  31524  dropab2  31525  mullimc  31788  mullimcf  31795  fourierdlem42  32097  fourierdlem48  32103  fourierdlem50  32105  fourierdlem51  32106  fourierdlem54  32109  fourierdlem86  32141  dfdfat2  32382  pfxeq  32579  2ffzoeq  32661  spthdifv  32670  usgra2pth  32672  edgssv2ALT  32719  edgssv2  32720  isfusgra0  32743  fusgraimpclALT2  32749  mgmhmpropd  32791  ismhm0  32811  isrnghm  32898  rngcsect  32988  rngcinv  32989  rngcsectALTV  33000  rngcinvALTV  33001  ringcsect  33039  ringcinv  33040  ringcsectALTV  33063  ringcinvALTV  33064  lmod1  33293  elbigo2  33373  bnj956  34182  bnj1146  34197  bnj18eq1  34332  bj-axrep1  34721  bj-axrep2  34722  bj-axrep3  34723  bj-axsep  34726  bj-eleq1w  34769  bj-rabeqd  34835  bj-axsep2  34840  islshpat  35155  lcvbr  35159  lshpsmreu  35247  ldual1dim  35304  cvrval  35407  cvrnbtwn3  35414  iscvlat2N  35462  ishlat3N  35492  hlrelat5N  35538  3dim0  35594  llnexatN  35658  islpln5  35672  islvol5  35716  pmapjat1  35990  ltrnu  36258  cdleme02N  36360  cdlemg33b  36846  cdlemg33c  36847  dvhb1dimN  37125  dibelval3  37287  dibopelval3  37288  dib1dim  37305  dibglbN  37306  diblsmopel  37311  dicval  37316  dicopelval  37317  dicelval3  37320  dicelval1sta  37327  dihopelvalcpre  37388  dih1dimatlem  37469  dihpN  37476  dihjatcclem4  37561  lpolsetN  37622  mapdpglem3  37815  hdmapglem7a  38070  ifpbi2  38113  iunrelexpmin1  38225
  Copyright terms: Public domain W3C validator