Theorem anim2d 611

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

Hypothesis

Ref	Expression
anim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
anim2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 608	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sbimdvOLD  2470  sbimdOLD  2472  darii  2724  festino  2733  baroco  2735  moeq3  3639  ssel  3883  sscon  4036  uniss  4766  trel3  5071  ssopab2  5323  coss1  5612  fununi  6299  imadif  6308  fss  6395  ssimaex  6615  ssoprab2  7081  poxp  7675  soxp  7676  suppofssd  7718  pmss12g  8283  ss2ixp  8323  xpdom2  8459  fisup2g  8778  fisupcl  8779  fiinf2g  8810  inf3lem1  8937  epfrs  9019  cfub  9517  cflm  9518  fin23lem34  9614  isf32lem2  9622  axcc4  9707  domtriomlem  9710  ltexprlem3  10306  nnunb  11741  indstr  12165  qbtwnxr  12443  qsqueeze  12444  xrsupsslem  12550  xrinfmsslem  12551  ioc0  12635  climshftlem  14765  o1rlimmul  14809  ramub2  16179  monmat2matmon  21116  tgcl  21261  neips  21405  ssnei2  21408  tgcnp  21545  cnpnei  21556  cnpco  21559  hauscmplem  21698  hauscmp  21699  llyss  21771  nllyss  21772  lfinun  21817  kgen2ss  21847  txcnpi  21900  txcmplem1  21933  fgss  22165  cnpflf2  22292  fclsss1  22314  fclscf  22317  alexsubALT  22343  cnextcn  22359  tsmsxp  22446  mopni3  22787  psmetutop  22860  tngngp3  22948  iscau4  23565  caussi  23583  ovolgelb  23764  mbfi1flim  24007  ellimc3  24160  lhop1  24294  tgbtwndiff  25974  axcontlem4  26436  sspmval  28201  shmodsi  28857  atcvat4i  29865  cdj3lem2b  29905  ifeqeqx  29986  acunirnmpt  30094  xrge0infss  30172  crefss  30730  issgon  30999  cvmlift2lem12  32169  satfv1  32218  satfvsucsuc  32220  ss2mcls  32423  poseq  32704  btwndiff  33097  seglecgr12im  33180  fnessref  33314  waj-ax  33371  lukshef-ax2  33372  icorempo  34163  finxpreclem1  34201  fvineqsneq  34224  pibt2  34229  tan2h  34415  poimirlem31  34454  poimir  34456  mblfinlem3  34462  mblfinlem4  34463  ismblfin  34464  cvrat4  36110  athgt  36123  ps-2  36145  paddss1  36484  paddss2  36485  cdlemg33b0  37368  cdlemg33a  37373  dihjat1lem  38095  fphpdo  38899  irrapxlem2  38905  pell14qrss1234  38938  pell1qrss14  38950  acongtr  39060  grumnudlem  40118  ax6e2eq  40430  islptre  41442  limccog  41443