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

Theorem anbi1d 716
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 26 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 650 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  anbi1  718  anbi12d  722  bi2anan9  889  pm5.71  952  cador  1521  drsb1  2216  eleq1d  2523  rexeqf  2995  reueq1f  2996  rmoeq1f  2997  rabeqf  3048  vtocl2gaf  3125  vtocl4ga  3130  alexeqg  3179  elrabi  3204  reu2eqd  3246  sbc2or  3287  sbc5  3303  rexss  3507  psstr  3548  ineq1  3638  difin2  3716  r19.28z  3872  r19.28zv  3875  rabsnifsb  4052  ssunsn2  4143  preq12bg  4167  prel12g  4168  opeq1  4179  eluni  4214  csbuni  4239  disjxun  4413  mpteq12f  4492  axrep1  4529  axrep2  4530  axrep3  4531  zfrepclf  4534  axsep  4537  axsep2  4539  zfauscl  4540  reusv2lem4  4620  rabxfrd  4634  opthg  4690  otthg  4698  copsexg  4700  euotd  4715  elopab  4722  pocl  4780  xpeq1  4866  elxpi  4868  vtoclr  4897  opbrop  4932  opelresg  5130  resopab2  5171  dflim2  5497  fun11  5669  feq2  5732  f1eq2  5797  f1eq3  5798  foeq2  5812  brprcneu  5880  ssimaexg  5953  dmfco  5961  fndmdif  6008  respreima  6031  isoeq5  6238  isoini  6253  isopolem  6260  f1oiso  6266  f1oiso2  6267  riotaeqdv  6277  oprabid  6341  oprabv  6365  mpt2eq123  6376  mpt2eq123dva  6378  eloprabga  6409  resoprab  6418  resoprab2  6419  elrnmpt2res  6436  ov  6442  ov3  6459  ov6g  6460  ovg  6461  caoftrn  6592  uniuni  6626  limuni3  6705  elxp4  6763  elxp5  6764  opabex3d  6797  opabex3  6798  opiota  6878  eloprabi  6881  cnvf1o  6921  frxp  6932  xporderlem  6933  poxp  6934  fnwelem  6937  suppimacnv  6951  rexsupp  6959  mpt2curryd  7041  smoel2  7107  omeu  7311  oeeui  7328  omabs  7373  omopth  7384  qliftel  7471  brecop  7481  eroveu  7483  erov  7485  ecopovtrn  7491  ixpsnf1o  7587  dom2lem  7634  xpsnen  7681  xpassen  7691  pw2f1olem  7701  xpf1o  7759  unxpdom  7804  domunfican  7869  preleq  8147  zfinf  8169  cantnfs  8196  tcvalg  8247  r0weon  8468  fseqenlem1  8480  acni2  8502  aceq1  8573  aceq0  8574  dfac2a  8585  dfac12lem2  8599  cardcf  8707  cfeq0  8711  cfsuc  8712  cff1  8713  cfss  8720  isf32lem5  8812  fin1a2lem6  8860  zfac  8915  brdom7disj  8984  brdom6disj  8985  axrepnd  9044  axunndlem1  9045  axinfnd  9056  axacndlem5  9061  axacnd  9062  zfcndrep  9064  zfcndinf  9068  zfcndac  9069  pwfseqlem4a  9111  pwfseqlem4  9112  gruina  9268  grothomex  9279  ordpipq  9392  elnpi  9438  genpass  9459  ltprord  9480  reclem2pr  9498  reclem3pr  9499  recexpr  9501  addsrmo  9522  mulsrmo  9523  addsrpr  9524  mulsrpr  9525  ltsosr  9543  mulgt0sr  9554  supsr  9561  ltresr  9589  axpre-lttrn  9615  axpre-mulgt0  9617  prime  11044  peano5uzti  11053  rexuz  11237  ltxr  11443  qbtwnre  11520  xmulneg1  11583  supxr2  11627  ixxval  11671  fzval  11814  preduz  11941  nn0opth2  12489  hashbclem  12647  hashf1lem2  12651  eqwrd  12743  swrdeq  12836  wrd2ind  12870  cshwcsh2id  12963  cleq1lem  13094  rtrclreclem3  13171  rtrclreclem4  13172  relexpindlem  13174  abslt  13425  absle  13426  lenegsq  13431  abs2difabs  13445  ello12  13628  elo12  13639  o1lo1  13649  rlimuni  13662  lo1resb  13676  o1resb  13678  2clim  13684  rlimcn2  13702  climcn2  13704  addcn2  13705  mulcn2  13707  o1of2  13724  sumeq1  13803  fsum2dlem  13879  modfsummod  13902  prodeq1f  14010  fprod2dlem  14082  znnenlem  14312  nndivdvds  14359  divalg2  14434  smupval  14510  gcdval  14518  gcdass  14561  lcmval  14603  lcmvalOLD  14604  lcmass  14627  rpexp  14720  pythagtriplem2  14815  pythagtrip  14832  vdwapun  14972  0ram  15026  ramub1lem2  15033  pwsle  15438  imasleval  15495  ismre  15544  ismri  15585  iscatd2  15635  dfiso2  15725  isssc  15773  funcpropd  15853  fullpropd  15873  fthres2b  15883  fthres2c  15884  setcsect  16032  prslem  16224  drsdir  16228  posi  16243  tosso  16330  ipoval  16448  ipolt  16453  odudlatb  16490  dirge  16531  gsumpropd2lem  16564  issgrpv  16577  issgrpn0  16578  mhmpropd  16636  mrcmndind  16661  mgmnsgrpex  16713  issubg3  16883  isga  16993  symgfixelq  17122  psgnfval  17189  psgnval  17196  isslw  17308  dprdw  17690  subgdmdprd  17715  drngpropd  18050  issubrg  18056  islmod  18143  lmodlema  18144  lmodprop2d  18198  lsslss  18232  lbspropd  18370  lbsacsbs  18427  aspval2  18619  psrbag  18636  pf1ind  18991  znleval  19173  islbs4  19438  islinds3  19440  mdetunilem4  19688  mdetunilem9  19693  istopg  19973  basis2  20014  tg2  20028  iscld  20090  neival  20166  isnei  20167  isneip  20169  neiptoptop  20195  neiptopnei  20196  neitr  20244  restlp  20247  iscn  20299  cnpval  20300  iscnp  20301  regsep  20398  nrmsep3  20419  1stcclb  20507  2ndc1stc  20514  2ndcctbss  20518  2ndcdisj  20519  llyi  20537  nllyi  20538  hausmapdom  20563  locfinnei  20586  comppfsc  20595  elkgen  20599  txbas  20630  txcls  20667  txcnpi  20671  ptpjopn  20675  txdis1cn  20698  txtube  20703  txcmplem1  20704  hausdiag  20708  tx1stc  20713  txkgen  20715  xkococnlem  20722  xkococn  20723  elqtop  20760  kqreglem1  20804  elmptrab  20890  isfbas  20892  elflim2  21027  elflim  21034  hauspwpwf1  21050  alexsublem  21107  ghmcnp  21177  qustgplem  21183  tsmssubm  21205  elutop  21296  ustuqtop4  21307  isucn  21341  iscfilu  21351  ispsmet  21368  ismet  21386  isxmet  21387  ismet2  21396  imasdsf1olem  21436  blres  21494  elmopn  21505  mopni  21555  neibl  21564  nrmmetd  21637  ngppropd  21693  elcncf  21969  mulc1cncf  21985  elpi1  22124  metcld2  22324  pmltpclem1  22447  ovolval  22474  ovolvalOLD  22475  itg1climres  22720  itg2val  22734  isibl  22771  itgeq1f  22777  itgresr  22784  iblcn  22804  itgfsum  22832  dvreslem  22912  dvfsumlem2  23027  deg1ldg  23089  vieta1  23313  ulm2  23388  sincosq2sgn  23502  sincosq4sgn  23504  efopn  23651  dvdsflsumcom  24165  fsumvma2  24190  logfac2  24193  dchrptlem1  24240  lgsdchrval  24323  pntibndlem3  24478  pntlemi  24490  pntleme  24494  pnt3  24498  istrkgld  24555  istrkg2ld  24556  istrkg3ld  24557  axtgsegcon  24560  axtg5seg  24561  axtgpasch  24563  axtgupdim2  24567  legov  24678  islnopp  24829  ishpg  24849  iscgra1  24900  brcgr  24978  brbtwn2  24983  axsegconlem1  24995  axsegcon  25005  axcontlem10  25051  usgra2edg  25157  trls  25314  istrl2  25316  trlon  25318  is2wlk  25343  spths  25345  0spth  25349  pthon  25353  spthon  25360  isspthonpth  25362  usgra2wlkspthlem1  25395  0crct  25402  0cycl  25403  usgrcyclnl2  25417  wwlknprop  25462  vfwlkniswwlkn  25482  wwlknext  25500  wwlknfi  25514  clwlk  25529  isclwlk  25532  clwlkcompim  25540  clwwlkn2  25551  clwwlknimp  25552  clwwlkel  25569  clwwlkf  25570  clwwlkext2edg  25578  wwlkext2clwwlk  25579  wwlksubclwwlk  25580  erclwwlknsym  25602  erclwwlkntr  25603  clwlkfoclwwlk  25621  el2wlkonotot0  25648  2spontn0vne  25663  rusgranumwlkl1  25723  rusgranumwlklem3  25727  rusgranumwlkb0  25729  rusgra0edg  25731  eupath2lem2  25754  3cyclfrgrarn1  25788  4cycl2vnunb  25793  frg2wot1  25833  usg2spot2nb  25841  extwwlkfablem2  25854  numclwwlkovfel2  25859  numclwwlkovf2  25860  numclwwlkovf2ex  25862  numclwwlkovgel  25864  numclwwlkovgelim  25865  numclwlk2lem2f  25879  numclwlk2lem2f1o  25881  numclwwlk5  25888  drngoi  26183  rngosn3  26202  vci  26215  isvclem  26244  nmoofval  26451  isph  26511  norm3lemt  26853  isch2  26924  cmbr  27285  eigre  27536  eigorth  27539  nmopub  27609  nmfnleub  27626  cvbr  27983  mdbr  27995  dmdbr  28000  chrelat2  28071  mdsymlem2  28105  rexunirn  28175  ifeqeqx  28206  funcnvmptOLD  28318  funcnvmpt  28319  1stpreima  28335  fpwrelmapffslem  28365  isomnd  28512  archirng  28553  isslmd  28566  slmdlema  28567  orngmul  28614  dya2iocuni  29153  omsfval  29166  omsfvalOLD  29170  elcarsg  29185  itgeq12dv  29207  isrrvv  29324  istrkg2d  29531  axtgupdim2OLD  29533  brafs  29537  bnj956  29636  bnj1146  29651  bnj18eq1  29786  kur14  29987  pconcn  29995  cnpcon  30001  txpcon  30003  cvmscbv  30029  cvmcov  30034  cvmsi  30036  cvmsval  30037  cvmopnlem  30049  cvmlift2lem10  30083  cvmlift3lem2  30091  cvmlift3lem6  30095  cvmlift3lem7  30096  cvmlift3lem9  30098  cvmlift3  30099  mclsssvlem  30248  mclsind  30256  eldm3  30450  opelco3  30468  fv1stcnv  30470  fv2ndcnv  30471  dfon2lem6  30482  dfon2lem7  30483  dfon2lem8  30484  dfon2  30486  poseq  30539  soseq  30540  sltval  30582  nodenselem5  30622  nocvxminlem  30627  elfuns  30730  brsuccf  30756  brofs  30820  5segofs  30821  brifs  30858  ifscgr  30859  brcolinear  30874  lineext  30891  brfs  30894  fscgr  30895  linecgr  30896  btwnconn1lem4  30905  btwnconn1lem8  30909  btwnconn1lem11  30912  btwnconn1lem12  30913  segcon2  30920  brsegle  30923  outsideofeq  30945  funray  30955  funline  30957  fvline  30959  linethru  30968  trer  31020  finminlem  31022  ivthALT  31039  filnetlem4  31085  bj-axrep1  31447  bj-axrep2  31448  bj-axrep3  31449  bj-axsep  31452  bj-eleq1w  31499  bj-ax8  31539  bj-rabeqd  31567  bj-axsep2  31572  csboprabg  31775  topdifinffinlem  31794  icoreval  31800  isbasisrelowllem1  31802  isbasisrelowllem2  31803  relowlssretop  31810  wl-ax11-lem8  31966  ptrest  31983  poimirlem1  31985  poimirlem13  31997  poimirlem14  31998  poimirlem22  32006  poimirlem24  32008  poimirlem26  32010  poimirlem27  32011  heicant  32019  mblfinlem3  32023  mblfinlem4  32024  mbfresfi  32031  itg2addnclem3  32039  itg2addnc  32040  itg2gt0cn  32041  areacirclem5  32080  cover2  32084  cover2g  32085  fdc  32118  fdc1  32119  heibor1  32186  bfp  32200  isdrngo1  32239  isriscg  32267  isfldidl2  32346  islshpat  32627  lcvbr  32631  lshpsmreu  32719  ldual1dim  32776  cvrval  32879  cvrnbtwn3  32886  iscvlat2N  32934  ishlat3N  32964  hlrelat5N  33010  3dim0  33066  llnexatN  33130  islpln5  33144  islvol5  33188  pmapjat1  33462  ltrnu  33730  cdleme02N  33832  cdlemg33b  34318  cdlemg33c  34319  dvhb1dimN  34597  dibelval3  34759  dibopelval3  34760  dib1dim  34777  dibglbN  34778  diblsmopel  34783  dicval  34788  dicopelval  34789  dicelval3  34792  dicelval1sta  34799  dihopelvalcpre  34860  dih1dimatlem  34941  dihpN  34948  dihjatcclem4  35033  lpolsetN  35094  mapdpglem3  35287  hdmapglem7a  35542  mrefg2  35593  mzpclval  35611  eldiophb  35643  eldioph2lem1  35646  eldioph3  35652  lzenom  35656  diophin  35659  eldiophss  35661  diophrex  35662  eq0rabdioph  35663  pellexlem3  35719  elpell1qr  35737  elpell14qr  35739  elpell1234qr  35741  jm2.27  35907  rmydioph  35913  expdiophlem1  35920  expdioph  35922  pw2f1ocnv  35936  hbtlem1  36026  hbtlem7  36028  dgraalem  36051  dgraalemOLD  36052  dgraaub  36057  dgraaubOLD  36058  ifpbi2  36154  inintabd  36229  cnvcnvintabd  36250  cnvintabd  36253  clcnvlem  36274  iunrelexpmin1  36344  binomcxplemnotnn0  36748  2sbc6g  36809  2sbc5g  36810  iotasbc  36813  dropab1  36843  dropab2  36844  disjinfi  37505  mapsnend  37517  mullimc  37733  mullimcf  37740  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem48  38055  fourierdlem50  38057  fourierdlem51  38058  fourierdlem54  38061  fourierdlem86  38093  ovnval2  38404  ovnsubaddlem1  38429  hoiqssbl  38484  dfdfat2  38670  pfxeq  38984  mptmpt2opabbrd  39075  2ffzoeq  39105  edgassv2  39328  uhgr2edg  39338  isfusgrf1  39436  edgnbusgreu  39490  cplgr3v  39551  vtxduhgrun  39587  upgr2wlk  39714  upgrtrls  39735  upgristrl  39736  upgrf1istrl  39737  2pthnloop  39763  isclWlke  39803  0Trl  39837  0spth-av  39841  0clWlk  39845  0Crct  39847  0Cycl  39848  2pthon3v-av  39891  upgr4cycl4dv4e  39925  spthdifv  39938  usgra2pth  39940  edgssv2ALT  39985  edgssv2  39986  isfusgra0  40009  fusgraimpclALT2  40015  mgmhmpropd  40057  ismhm0  40077  isrnghm  40164  rngcsect  40254  rngcinv  40255  rngcsectALTV  40266  rngcinvALTV  40267  ringcsect  40305  ringcinv  40306  ringcsectALTV  40329  ringcinvALTV  40330  lmod1  40557  elbigo2  40635
  Copyright terms: Public domain W3C validator