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  2071  eleq1  2464  rexeqf  2861  reueq1f  2862  rmoeq1f  2863  rabeqf  2909  vtocl2gaf  2978  alexeq  3025  ceqex  3026  elrabi  3050  sbc2or  3129  sbc5  3145  rexss  3370  psstr  3411  ineq1  3495  difin2  3563  r19.28z  3680  r19.28zv  3683  ssunsn2  3918  preq12bg  3937  opeq1  3944  eluni  3978  disjxun  4170  mpteq12f  4245  axrep1  4281  axrep2  4282  axrep3  4283  zfrepclf  4286  axsep  4289  axsep2  4291  zfauscl  4292  opthg  4396  copsexg  4402  euotd  4417  elopab  4422  pocl  4470  dflim2  4597  uniuni  4675  reusv2lem4  4686  rabxfrd  4703  limuni3  4791  xpeq1  4851  elxpi  4853  vtoclr  4881  opbrop  4914  opelresg  5112  resopab2  5149  elxp4  5316  elxp5  5317  fun11  5475  feq2  5536  f1eq2  5594  f1eq3  5595  foeq2  5609  brprcneu  5680  ssimaexg  5748  dmfco  5756  fndmdif  5793  rexsupp  5814  respreima  5818  opabex3d  5948  opabex3  5949  isoeq5  6002  isoini  6017  isopolem  6024  f1oiso  6030  f1oiso2  6031  oprabid  6064  mpt2eq123  6092  mpt2eq123dva  6094  eloprabga  6119  resoprab  6125  resoprab2  6126  ov  6152  ov3  6169  ov6g  6170  ovg  6171  caoftrn  6298  eloprabi  6372  cnvf1o  6404  frxp  6415  xporderlem  6416  poxp  6417  fnwelem  6420  opiota  6494  riotaeqdv  6509  smoel2  6584  omeu  6787  oeeui  6804  omabs  6849  omopth  6860  qliftel  6946  brecop  6956  eroveu  6958  erov  6960  ecopovtrn  6966  th3qlem2  6970  th3q  6972  ixpsnf1o  7061  dom2lem  7106  xpsnen  7151  xpassen  7161  pw2f1olem  7171  xpf1o  7228  unxpdom  7275  domunfican  7338  preleq  7528  zfinf  7550  cantnfs  7577  tcvalg  7633  r0weon  7850  fseqenlem1  7861  acni2  7883  aceq1  7954  aceq0  7955  dfac2a  7966  dfac12lem2  7980  cardcf  8088  cfeq0  8092  cfsuc  8093  cff1  8094  cfss  8101  isf32lem5  8193  fin1a2lem6  8241  zfac  8296  brdom7disj  8365  brdom6disj  8366  axrepnd  8425  axunndlem1  8426  axinfnd  8437  axacndlem5  8442  axacnd  8443  zfcndrep  8445  zfcndinf  8449  zfcndac  8450  pwfseqlem4a  8492  pwfseqlem4  8493  gruina  8649  grothomex  8660  ordpipq  8775  elnpi  8821  genpass  8842  ltprord  8863  reclem2pr  8881  reclem3pr  8882  recexpr  8884  ltsosr  8925  mulgt0sr  8936  supsr  8943  ltresr  8971  axpre-lttrn  8997  axpre-mulgt0  8999  prime  10306  peano5uzti  10315  uzindOLD  10320  rexuz  10483  ltxr  10671  qbtwnre  10741  xmulneg1  10804  supxr2  10848  ixxval  10880  fzval  11001  nn0opth2  11520  hashbclem  11656  hashf1lem2  11660  abslt  12073  absle  12074  lenegsq  12079  abs2difabs  12093  ello12  12265  elo12  12276  o1lo1  12286  rlimuni  12299  lo1resb  12313  o1resb  12315  2clim  12321  rlimcn2  12339  climcn2  12341  addcn2  12342  mulcn2  12344  o1of2  12361  sumeq1f  12437  fsum2dlem  12509  znnenlem  12766  nndivdvds  12813  divalg2  12880  smupval  12955  gcdval  12963  gcdass  13000  rpexp  13075  pythagtriplem2  13146  pythagtrip  13163  vdwapun  13297  0ram  13343  ramub1lem2  13350  pwsle  13669  imasleval  13721  ismre  13770  ismri  13811  iscatd2  13861  isssc  13975  funcpropd  14052  fullpropd  14072  fthres2b  14082  fthres2c  14083  setcsect  14199  prslem  14343  drsdir  14347  posi  14362  tosso  14420  ipoval  14535  ipolt  14540  odudlatb  14577  dirge  14637  mndpropd  14676  mhmpropd  14699  issubg3  14915  isga  15023  isslw  15197  dprdw  15523  subgdmdprd  15547  drngpropd  15817  issubrg  15823  islmod  15909  lmodlema  15910  lmodprop2d  15961  lsslss  15992  lbspropd  16126  lbsacsbs  16183  aspval2  16360  psrbag  16386  znleval  16790  istopg  16923  basis2  16971  tg2  16985  iscld  17046  neival  17121  isnei  17122  isneip  17124  neiptoptop  17150  neiptopnei  17151  neitr  17198  restlp  17201  iscn  17253  cnpval  17254  iscnp  17255  regsep  17352  nrmsep3  17373  1stcclb  17460  2ndc1stc  17467  2ndcctbss  17471  2ndcdisj  17472  llyi  17490  nllyi  17491  hausmapdom  17516  elkgen  17521  txbas  17552  txcls  17589  txcnpi  17593  ptpjopn  17597  txdis1cn  17620  txtube  17625  txcmplem1  17626  hausdiag  17630  tx1stc  17635  txkgen  17637  xkococnlem  17644  xkococn  17645  elqtop  17682  kqreglem1  17726  elmptrab  17812  isfbas  17814  elflim2  17949  elflim  17956  hauspwpwf1  17972  alexsublem  18028  ghmcnp  18097  divstgplem  18103  tsmssubm  18125  elutop  18216  ustuqtop4  18227  isucn  18261  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  ismet2  18316  imasdsf1olem  18356  blres  18414  elmopn  18425  mopni  18475  neibl  18484  nrmmetd  18575  ngppropd  18631  elcncf  18872  mulc1cncf  18888  elpi1  19023  metcld2  19212  pmltpclem1  19298  ovolval  19323  itg1climres  19559  itg2val  19573  isibl  19610  itgeq1f  19616  itgresr  19623  iblcn  19643  itgfsum  19671  dvreslem  19749  dvfsumlem2  19864  pf1ind  19928  deg1ldg  19968  vieta1  20182  ulm2  20254  sincosq2sgn  20360  sincosq4sgn  20362  efopn  20502  dvdsflsumcom  20926  fsumvma2  20951  logfac2  20954  dchrptlem1  21001  lgsdchrval  21084  pntibndlem3  21239  pntlemi  21251  pntleme  21255  pnt3  21259  usgra2edg  21355  trls  21489  istrl2  21491  trlon  21493  is2wlk  21518  spths  21520  0spth  21524  pthon  21528  spthon  21535  isspthonpth  21537  0crct  21566  0cycl  21567  usgrcyclnl2  21581  eupath2lem2  21653  drngoi  21948  rngosn3  21967  vci  21980  isvclem  22009  nmoofval  22216  isph  22276  norm3lemt  22607  isch2  22679  cmbr  23039  eigre  23291  eigorth  23294  nmopub  23364  nmfnleub  23381  cvbr  23738  mdbr  23750  dmdbr  23755  chrelat2  23826  mdsymlem2  23860  rexunirn  23931  ifeqeqx  23954  funcnvmptOLD  24035  funcnvmpt  24036  1stpreima  24048  gsumpropd2lem  24173  isofld  24188  ofldadd  24191  ofldmul  24192  dya2iocuni  24586  itgeq12dv  24594  isrrvv  24654  kur14  24855  pconcn  24864  cnpcon  24870  txpcon  24872  cvmscbv  24898  cvmcov  24903  cvmsi  24905  cvmsval  24906  cvmopnlem  24918  cvmlift2lem10  24952  cvmlift3lem2  24960  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  cvmlift3  24968  relexp0  25082  relexpsucr  25083  relexpsucl  25085  relexpcnv  25086  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  rtrclreclem.trans  25099  rtrclreclem.min  25100  prodeq1f  25187  fprod2dlem  25257  eldm3  25333  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  dfon2  25362  preduz  25414  poseq  25467  soseq  25468  sltval  25515  nodenselem5  25553  nocvxminlem  25558  brimg  25690  brcgr  25743  brbtwn2  25748  axsegconlem1  25760  axsegcon  25770  axcontlem10  25816  brofs  25843  5segofs  25844  brifs  25881  ifscgr  25882  brcolinear  25897  lineext  25914  brfs  25917  fscgr  25918  linecgr  25919  btwnconn1lem4  25928  btwnconn1lem8  25932  btwnconn1lem11  25935  btwnconn1lem12  25936  segcon2  25943  brsegle  25946  outsideofeq  25968  funray  25978  funline  25980  fvline  25982  linethru  25991  mblfinlem2  26144  mblfinlem3  26145  mbfresfi  26152  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  areacirclem6  26186  trer  26209  finminlem  26211  ivthALT  26228  locfinnei  26272  comppfsc  26277  filnetlem4  26300  cover2  26305  cover2g  26306  fdc  26339  fdc1  26340  heibor1  26409  bfp  26423  isdrngo1  26462  isriscg  26490  isfldidl2  26569  mrefg2  26651  mzpclval  26672  eldiophb  26705  eldioph2lem1  26708  eldioph3  26714  lzenom  26718  diophin  26721  eldiophss  26723  diophrex  26724  eq0rabdioph  26725  pellexlem3  26784  elpell1qr  26800  elpell14qr  26802  elpell1234qr  26804  jm2.27  26969  rmydioph  26975  expdiophlem1  26982  expdioph  26984  pw2f1ocnv  26998  islbs4  27170  islinds3  27172  hbtlem1  27195  hbtlem7  27197  dgraalem  27218  dgraaub  27221  psgnfval  27291  psgnval  27298  2sbc6g  27483  2sbc5g  27484  iotasbc  27487  dropab1  27517  dropab2  27518  dfdfat2  27862  otthg  27952  swrdccatin12  28026  usgra2wlkspthlem1  28036  spthdifv  28039  usgra2pth  28041  el2wlkonotot0  28069  2spontn0vne  28084  3cyclfrgrarn1  28116  4cycl2vnunb  28121  frg2wot1  28160  usg2spot2nb  28168  bnj956  28853  bnj1146  28868  bnj18eq1  29004  drsb1NEW7  29212  islshpat  29500  lcvbr  29504  lshpsmreu  29592  ldual1dim  29649  cvrval  29752  cvrnbtwn3  29759  iscvlat2N  29807  ishlat3N  29837  hlrelat5N  29883  3dim0  29939  llnexatN  30003  islpln5  30017  islvol5  30061  pmapjat1  30335  ltrnu  30603  cdleme02N  30704  cdlemg33b  31189  cdlemg33c  31190  dvhb1dimN  31468  dibelval3  31630  dibopelval3  31631  dib1dim  31648  dibglbN  31649  diblsmopel  31654  dicval  31659  dicopelval  31660  dicelval3  31663  dicelval1sta  31670  dihopelvalcpre  31731  dih1dimatlem  31812  dihpN  31819  dihjatcclem4  31904  lpolsetN  31965  mapdpglem3  32158  hdmapglem7a  32413
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