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

Theorem anim1ci 617
 Description: Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.)
Hypothesis
Ref Expression
anim1i.1 (𝜑𝜓)
Assertion
Ref Expression
anim1ci ((𝜑𝜒) → (𝜒𝜓))

Proof of Theorem anim1ci
StepHypRef Expression
1 anim1i.1 . 2 (𝜑𝜓)
2 id 22 . 2 (𝜒𝜒)
31, 2anim12ci 615 1 ((𝜑𝜒) → (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  norassOLD  1530  elpwdifsn  4720  f1ocnv  6626  frnssb  6884  dfrecs3  8008  odi  8204  snmapen  8589  infcntss  8791  lediv2a  11533  lbreu  11590  nn2ge  11663  dfceil2  13208  leexp1a  13538  faclbnd6  13658  ccatval3  13932  ccatalpha  13946  ccatswrd  14029  pfxccatin12lem2  14092  pfxccat3  14095  pfxccat3a  14099  repsdf2  14139  repswsymball  14140  dvdsdivcl  15665  nn0ehalf  15728  nn0oddm1d2  15735  nnoddm1d2  15736  sumeven  15737  ndvdssub  15759  coprmgcdb  15992  ncoprmgcdne1b  15993  divgcdcoprm0  16008  ncoprmlnprm  16067  vfermltl  16137  powm2modprm  16139  modprmn0modprm0  16143  dvdsprmpweqle  16221  prmgaplem4  16389  prmgaplem7  16392  cshwshashlem2  16429  efmndid  18052  efmndmnd  18053  gimcnv  18406  cygabl  19009  gsummptnn0fz  19105  lmimcnv  19838  ixpsnbasval  19981  matbas2  21029  scmatmats  21119  scmatscm  21121  scmatmulcl  21126  scmatf  21137  mdet1  21209  mdet0  21214  cramerimplem1  21291  cramer  21299  decpmatmul  21379  pmatcollpwscmat  21398  chfacfisf  21461  dv11cn  24597  logbgcd1irr  25371  lnhl  26400  usgrfilem  27108  cplgr3v  27216  wlkreslem  27450  usgr2trlncl  27540  wwlksnextbi  27671  clwwlkccatlem  27766  clwwlkel  27824  clwwlknon1loop  27876  uhgr3cyclex  27960  eucrctshift  28021  1to3vfriswmgr  28058  frgrnbnb  28071  fusgreghash2wspv  28113  numclwwlk6  28168  frgrreggt1  28171  frgrregord013  28173  hhcmpl  28976  upgracycumgr  32400  bj-finsumval0  34566  indexa  35007  founiiun0  41449  or2expropbilem1  43266  fundmdfat  43327  reuopreuprim  43687  elbigolo1  44616  2sphere  44735  itsclquadb  44762
 Copyright terms: Public domain W3C validator