Theorem anim2d 575

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
anim1d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
anim2d	|- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 24	. 2 |- ( ph -> ( th -> th ) )
2		anim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	anim12d 572	1 |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 376

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 378

This theorem is referenced by:  eleq2dOLD  2535  moeq3  3203  ssel  3412  sscon  3556  uniss  4211  trel3  4498  ssopab2  4727  coss1  4995  fununi  5659  imadif  5668  fss  5749  ssimaex  5945  ssoprab2  6366  poxp  6927  soxp  6928  pmss12g  7516  ss2ixp  7553  xpdom2  7685  fisup2g  8002  fisupcl  8003  fiinf2g  8034  inf3lem1  8151  epfrs  8233  cfub  8697  cflm  8698  fin23lem34  8794  isf32lem2  8802  axcc4  8887  domtriomlem  8890  ltexprlem3  9481  nnunb  10889  indstr  11250  qbtwnxr  11516  qsqueeze  11517  xrsupsslem  11617  xrinfmsslem  11618  ioc0  11708  climshftlem  13715  o1rlimmul  13759  ramub2  15050  monmat2matmon  19925  tgcl  20062  neips  20206  ssnei2  20209  tgcnp  20346  cnpnei  20357  cnpco  20360  hauscmplem  20498  hauscmp  20499  llyss  20571  nllyss  20572  lfinun  20617  kgen2ss  20647  txcnpi  20700  txcmplem1  20733  fgss  20966  cnpflf2  21093  fclsss1  21115  fclscf  21118  alexsubALT  21144  cnextcn  21160  tsmsxp  21247  mopni3  21587  psmetutop  21660  iscau4  22327  caussi  22345  ovolgelb  22511  mbfi1flim  22760  ellimc3  22913  lhop1  23045  tgbtwndiff  24629  axcontlem4  25076  iswlkg  25331  sspmval  26453  sspival  26458  shmodsi  27123  atcvat4i  28131  cdj3lem2b  28171  ifeqeqx  28236  acunirnmpt  28336  xrge0infss  28415  crefss  28750  issgon  29019  cvmlift2lem12  30109  ss2mcls  30278  poseq  30562  btwndiff  30865  seglecgr12im  30948  fnessref  31084  waj-ax  31145  lukshef-ax2  31146  icorempt2  31824  finxpreclem1  31851  tan2h  32001  poimirlem31  32035  poimir  32037  mblfinlem3  32043  mblfinlem4  32044  ismblfin  32045  cvrat4  33079  athgt  33092  ps-2  33114  paddss1  33453  paddss2  33454  cdlemg33b0  34339  cdlemg33a  34344  dihjat1lem  35067  fphpdo  35731  irrapxlem2  35738  pell14qrss1234  35773  pell1qrss14  35785  acongtr  35899  ax6e2eq  36994  islptre  37796  limccog  37797