Theorem anim2d 610

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 607	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  darii  2657  festino  2666  baroco  2668  moeq3  3717  sbcimdv  3861  ssel  3984  sscon  4146  uniss  4924  trel3  5281  ssopab2  5554  coss1  5864  fununi  6636  imadif  6645  fss  6746  ssimaex  6989  ssoprab2  7496  poxp  8147  soxp  8148  poseq  8177  suppofssd  8222  pmss12g  8902  ss2ixp  8943  xpdom2  9108  fisup2g  9512  fisupcl  9513  fiinf2g  9544  inf3lem1  9672  epfrs  9775  cfub  10293  cflm  10294  fin23lem34  10390  isf32lem2  10398  axcc4  10483  domtriomlem  10486  ltexprlem3  11082  nnunb  12524  indstr  12956  qbtwnxr  13237  qsqueeze  13238  xrsupsslem  13344  xrinfmsslem  13345  ioc0  13429  climshftlem  15589  o1rlimmul  15634  ramub2  17029  monmat2matmon  22817  tgcl  22963  neips  23108  ssnei2  23111  tgcnp  23248  cnpnei  23259  cnpco  23262  hauscmplem  23401  hauscmp  23402  llyss  23474  nllyss  23475  lfinun  23520  kgen2ss  23550  txcnpi  23603  txcmplem1  23636  fgss  23868  cnpflf2  23995  fclsss1  24017  fclscf  24020  alexsubALT  24046  cnextcn  24062  tsmsxp  24150  mopni3  24494  psmetutop  24567  tngngp3  24664  iscau4  25298  caussi  25316  ovolgelb  25500  mbfi1flim  25744  ellimc3  25899  lhop1  26038  tgbtwndiff  28475  axcontlem4  28943  clwwlknonwwlknonb  30081  sspmval  30708  shmodsi  31364  atcvat4i  32372  cdj3lem2b  32412  ifeqeqx  32509  acunirnmpt  32622  xrge0infss  32712  crefss  33740  issgon  34032  cvmlift2lem12  35227  satfv1  35276  satfvsucsuc  35278  ss2mcls  35481  btwndiff  35936  seglecgr12im  36019  fnessref  36155  waj-ax  36212  lukshef-ax2  36213  bj-isrvec  37086  icorempo  37143  finxpreclem1  37181  fvineqsneq  37204  pibt2  37209  tan2h  37398  poimirlem31  37437  poimir  37439  mblfinlem3  37445  mblfinlem4  37446  ismblfin  37447  cvrat4  39227  athgt  39240  ps-2  39262  paddss1  39601  paddss2  39602  cdlemg33b0  40485  cdlemg33a  40490  dihjat1lem  41212  fphpdo  42586  irrapxlem2  42592  pell14qrss1234  42625  pell1qrss14  42637  acongtr  42748  ofoaid1  43136  ofoaid2  43137  fzunt  43234  fzuntd  43235  fzunt1d  43236  fzuntgd  43237  grumnudlem  44071  ax6e2eq  44345  islptre  45351  limccog  45352  grilcbri2  47613  opnneilv  48364