Theorem anim2d 612

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  darii  2662  festino  2671  baroco  2673  moeq3  3720  sbcimdv  3864  ssel  3988  sscon  4152  uniss  4919  trel3  5274  axprlem4  5431  ssopab2  5555  coss1  5868  fununi  6642  imadif  6651  fss  6752  ssimaex  6993  ssoprab2  7500  poxp  8151  soxp  8152  poseq  8181  suppofssd  8226  pmss12g  8907  ss2ixp  8948  xpdom2  9105  fisup2g  9505  fisupcl  9506  fiinf2g  9537  inf3lem1  9665  epfrs  9768  cfub  10286  cflm  10287  fin23lem34  10383  isf32lem2  10391  axcc4  10476  domtriomlem  10479  ltexprlem3  11075  nnunb  12519  indstr  12955  qbtwnxr  13238  qsqueeze  13239  xrsupsslem  13345  xrinfmsslem  13346  ioc0  13430  climshftlem  15606  o1rlimmul  15651  ramub2  17047  monmat2matmon  22845  tgcl  22991  neips  23136  ssnei2  23139  tgcnp  23276  cnpnei  23287  cnpco  23290  hauscmplem  23429  hauscmp  23430  llyss  23502  nllyss  23503  lfinun  23548  kgen2ss  23578  txcnpi  23631  txcmplem1  23664  fgss  23896  cnpflf2  24023  fclsss1  24045  fclscf  24048  alexsubALT  24074  cnextcn  24090  tsmsxp  24178  mopni3  24522  psmetutop  24595  tngngp3  24692  iscau4  25326  caussi  25344  ovolgelb  25528  mbfi1flim  25772  ellimc3  25928  lhop1  26067  tgbtwndiff  28528  axcontlem4  28996  clwwlknonwwlknonb  30134  sspmval  30761  shmodsi  31417  atcvat4i  32425  cdj3lem2b  32465  ifeqeqx  32562  acunirnmpt  32675  xrge0infss  32770  crefss  33809  issgon  34103  cvmlift2lem12  35298  satfv1  35347  satfvsucsuc  35349  ss2mcls  35552  btwndiff  36008  seglecgr12im  36091  fnessref  36339  waj-ax  36396  lukshef-ax2  36397  bj-isrvec  37276  icorempo  37333  finxpreclem1  37371  fvineqsneq  37394  pibt2  37399  tan2h  37598  poimirlem31  37637  poimir  37639  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  cvrat4  39425  athgt  39438  ps-2  39460  paddss1  39799  paddss2  39800  cdlemg33b0  40683  cdlemg33a  40688  dihjat1lem  41410  fphpdo  42804  irrapxlem2  42810  pell14qrss1234  42843  pell1qrss14  42855  acongtr  42966  ofoaid1  43347  ofoaid2  43348  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  grumnudlem  44280  ax6e2eq  44554  modelaxreplem1  44942  islptre  45574  limccog  45575  grilcbri2  47906  opnneilv  48704