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  1400  drsb1  2102  eleq1  2495  rexeqf  2893  reueq1f  2894  rmoeq1f  2895  rabeqf  2941  vtocl2gaf  3010  alexeq  3057  ceqex  3058  elrabi  3082  sbc2or  3161  sbc5  3177  rexss  3402  psstr  3443  ineq1  3527  difin2  3595  r19.28z  3712  r19.28zv  3715  ssunsn2  3950  preq12bg  3969  opeq1  3976  eluni  4010  disjxun  4202  mpteq12f  4277  axrep1  4313  axrep2  4314  axrep3  4315  zfrepclf  4318  axsep  4321  axsep2  4323  zfauscl  4324  opthg  4428  copsexg  4434  euotd  4449  elopab  4454  pocl  4502  dflim2  4629  uniuni  4707  reusv2lem4  4718  rabxfrd  4735  limuni3  4823  xpeq1  4883  elxpi  4885  vtoclr  4913  opbrop  4946  opelresg  5144  resopab2  5181  elxp4  5348  elxp5  5349  fun11  5507  feq2  5568  f1eq2  5626  f1eq3  5627  foeq2  5641  brprcneu  5712  ssimaexg  5780  dmfco  5788  fndmdif  5825  rexsupp  5846  respreima  5850  opabex3d  5980  opabex3  5981  isoeq5  6034  isoini  6049  isopolem  6056  f1oiso  6062  f1oiso2  6063  oprabid  6096  mpt2eq123  6124  mpt2eq123dva  6126  eloprabga  6151  resoprab  6157  resoprab2  6158  ov  6184  ov3  6201  ov6g  6202  ovg  6203  caoftrn  6330  eloprabi  6404  cnvf1o  6436  frxp  6447  xporderlem  6448  poxp  6449  fnwelem  6452  opiota  6526  riotaeqdv  6541  smoel2  6616  omeu  6819  oeeui  6836  omabs  6881  omopth  6892  qliftel  6978  brecop  6988  eroveu  6990  erov  6992  ecopovtrn  6998  th3qlem2  7002  th3q  7004  ixpsnf1o  7093  dom2lem  7138  xpsnen  7183  xpassen  7193  pw2f1olem  7203  xpf1o  7260  unxpdom  7307  domunfican  7370  preleq  7561  zfinf  7583  cantnfs  7610  tcvalg  7666  r0weon  7883  fseqenlem1  7894  acni2  7916  aceq1  7987  aceq0  7988  dfac2a  7999  dfac12lem2  8013  cardcf  8121  cfeq0  8125  cfsuc  8126  cff1  8127  cfss  8134  isf32lem5  8226  fin1a2lem6  8274  zfac  8329  brdom7disj  8398  brdom6disj  8399  axrepnd  8458  axunndlem1  8459  axinfnd  8470  axacndlem5  8475  axacnd  8476  zfcndrep  8478  zfcndinf  8482  zfcndac  8483  pwfseqlem4a  8525  pwfseqlem4  8526  gruina  8682  grothomex  8693  ordpipq  8808  elnpi  8854  genpass  8875  ltprord  8896  reclem2pr  8914  reclem3pr  8915  recexpr  8917  ltsosr  8958  mulgt0sr  8969  supsr  8976  ltresr  9004  axpre-lttrn  9030  axpre-mulgt0  9032  prime  10339  peano5uzti  10348  uzindOLD  10353  rexuz  10516  ltxr  10704  qbtwnre  10774  xmulneg1  10837  supxr2  10881  ixxval  10913  fzval  11034  nn0opth2  11553  hashbclem  11689  hashf1lem2  11693  abslt  12106  absle  12107  lenegsq  12112  abs2difabs  12126  ello12  12298  elo12  12309  o1lo1  12319  rlimuni  12332  lo1resb  12346  o1resb  12348  2clim  12354  rlimcn2  12372  climcn2  12374  addcn2  12375  mulcn2  12377  o1of2  12394  sumeq1f  12470  fsum2dlem  12542  znnenlem  12799  nndivdvds  12846  divalg2  12913  smupval  12988  gcdval  12996  gcdass  13033  rpexp  13108  pythagtriplem2  13179  pythagtrip  13196  vdwapun  13330  0ram  13376  ramub1lem2  13383  pwsle  13702  imasleval  13754  ismre  13803  ismri  13844  iscatd2  13894  isssc  14008  funcpropd  14085  fullpropd  14105  fthres2b  14115  fthres2c  14116  setcsect  14232  prslem  14376  drsdir  14380  posi  14395  tosso  14453  ipoval  14568  ipolt  14573  odudlatb  14610  dirge  14670  mndpropd  14709  mhmpropd  14732  issubg3  14948  isga  15056  isslw  15230  dprdw  15556  subgdmdprd  15580  drngpropd  15850  issubrg  15856  islmod  15942  lmodlema  15943  lmodprop2d  15994  lsslss  16025  lbspropd  16159  lbsacsbs  16216  aspval2  16393  psrbag  16419  znleval  16823  istopg  16956  basis2  17004  tg2  17018  iscld  17079  neival  17154  isnei  17155  isneip  17157  neiptoptop  17183  neiptopnei  17184  neitr  17232  restlp  17235  iscn  17287  cnpval  17288  iscnp  17289  regsep  17386  nrmsep3  17407  1stcclb  17495  2ndc1stc  17502  2ndcctbss  17506  2ndcdisj  17507  llyi  17525  nllyi  17526  hausmapdom  17551  elkgen  17556  txbas  17587  txcls  17624  txcnpi  17628  ptpjopn  17632  txdis1cn  17655  txtube  17660  txcmplem1  17661  hausdiag  17665  tx1stc  17670  txkgen  17672  xkococnlem  17679  xkococn  17680  elqtop  17717  kqreglem1  17761  elmptrab  17847  isfbas  17849  elflim2  17984  elflim  17991  hauspwpwf1  18007  alexsublem  18063  ghmcnp  18132  divstgplem  18138  tsmssubm  18160  elutop  18251  ustuqtop4  18262  isucn  18296  iscfilu  18306  ispsmet  18323  ismet  18341  isxmet  18342  ismet2  18351  imasdsf1olem  18391  blres  18449  elmopn  18460  mopni  18510  neibl  18519  nrmmetd  18610  ngppropd  18666  elcncf  18907  mulc1cncf  18923  elpi1  19058  metcld2  19247  pmltpclem1  19333  ovolval  19358  itg1climres  19594  itg2val  19608  isibl  19645  itgeq1f  19651  itgresr  19658  iblcn  19678  itgfsum  19706  dvreslem  19784  dvfsumlem2  19899  pf1ind  19963  deg1ldg  20003  vieta1  20217  ulm2  20289  sincosq2sgn  20395  sincosq4sgn  20397  efopn  20537  dvdsflsumcom  20961  fsumvma2  20986  logfac2  20989  dchrptlem1  21036  lgsdchrval  21119  pntibndlem3  21274  pntlemi  21286  pntleme  21290  pnt3  21294  usgra2edg  21390  trls  21524  istrl2  21526  trlon  21528  is2wlk  21553  spths  21555  0spth  21559  pthon  21563  spthon  21570  isspthonpth  21572  0crct  21601  0cycl  21602  usgrcyclnl2  21616  eupath2lem2  21688  drngoi  21983  rngosn3  22002  vci  22015  isvclem  22044  nmoofval  22251  isph  22311  norm3lemt  22642  isch2  22714  cmbr  23074  eigre  23326  eigorth  23329  nmopub  23399  nmfnleub  23416  cvbr  23773  mdbr  23785  dmdbr  23790  chrelat2  23861  mdsymlem2  23895  rexunirn  23966  ifeqeqx  23989  funcnvmptOLD  24070  funcnvmpt  24071  1stpreima  24083  gsumpropd2lem  24208  isofld  24223  ofldadd  24226  ofldmul  24227  dya2iocuni  24621  itgeq12dv  24629  isrrvv  24689  kur14  24890  pconcn  24899  cnpcon  24905  txpcon  24907  cvmscbv  24933  cvmcov  24938  cvmsi  24940  cvmsval  24941  cvmopnlem  24953  cvmlift2lem10  24987  cvmlift3lem2  24995  cvmlift3lem6  24999  cvmlift3lem7  25000  cvmlift3lem9  25002  cvmlift3  25003  relexp0  25117  relexpsucr  25118  relexpsucl  25120  relexpcnv  25121  relexpdm  25123  relexprn  25124  relexpadd  25126  relexpindlem  25127  rtrclreclem.trans  25134  rtrclreclem.min  25135  prodeq1f  25223  fprod2dlem  25293  eldm3  25374  dfon2lem6  25399  dfon2lem7  25400  dfon2lem8  25401  dfon2  25403  preduz  25455  poseq  25508  soseq  25509  sltval  25556  nodenselem5  25594  nocvxminlem  25599  brcgr  25787  brbtwn2  25792  axsegconlem1  25804  axsegcon  25814  axcontlem10  25860  brofs  25887  5segofs  25888  brifs  25925  ifscgr  25926  brcolinear  25941  lineext  25958  brfs  25961  fscgr  25962  linecgr  25963  btwnconn1lem4  25972  btwnconn1lem8  25976  btwnconn1lem11  25979  btwnconn1lem12  25980  segcon2  25987  brsegle  25990  outsideofeq  26012  funray  26022  funline  26024  fvline  26026  linethru  26035  mblfinlem2  26191  mblfinlem3  26192  mbfresfi  26199  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  areacirclem6  26233  trer  26256  finminlem  26258  ivthALT  26275  locfinnei  26319  comppfsc  26324  filnetlem4  26347  cover2  26352  cover2g  26353  fdc  26386  fdc1  26387  heibor1  26456  bfp  26470  isdrngo1  26509  isriscg  26537  isfldidl2  26616  mrefg2  26698  mzpclval  26719  eldiophb  26752  eldioph2lem1  26755  eldioph3  26761  lzenom  26765  diophin  26768  eldiophss  26770  diophrex  26771  eq0rabdioph  26772  pellexlem3  26831  elpell1qr  26847  elpell14qr  26849  elpell1234qr  26851  jm2.27  27016  rmydioph  27022  expdiophlem1  27029  expdioph  27031  pw2f1ocnv  27045  islbs4  27217  islinds3  27219  hbtlem1  27242  hbtlem7  27244  dgraalem  27265  dgraaub  27268  psgnfval  27338  psgnval  27345  2sbc6g  27530  2sbc5g  27531  iotasbc  27534  dropab1  27564  dropab2  27565  dfdfat2  27909  otthg  28000  wrdeq0  28083  swrdccatin12  28101  usgra2wlkspthlem1  28180  spthdifv  28183  usgra2pth  28185  el2wlkonotot0  28213  2spontn0vne  28228  3cyclfrgrarn1  28260  4cycl2vnunb  28265  frg2wot1  28304  usg2spot2nb  28312  bnj956  29001  bnj1146  29016  bnj18eq1  29152  drsb1NEW7  29360  islshpat  29654  lcvbr  29658  lshpsmreu  29746  ldual1dim  29803  cvrval  29906  cvrnbtwn3  29913  iscvlat2N  29961  ishlat3N  29991  hlrelat5N  30037  3dim0  30093  llnexatN  30157  islpln5  30171  islvol5  30215  pmapjat1  30489  ltrnu  30757  cdleme02N  30858  cdlemg33b  31343  cdlemg33c  31344  dvhb1dimN  31622  dibelval3  31784  dibopelval3  31785  dib1dim  31802  dibglbN  31803  diblsmopel  31808  dicval  31813  dicopelval  31814  dicelval3  31817  dicelval1sta  31824  dihopelvalcpre  31885  dih1dimatlem  31966  dihpN  31973  dihjatcclem4  32058  lpolsetN  32119  mapdpglem3  32312  hdmapglem7a  32567
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