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 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  2668  festino  2677  baroco  2679  moeq3  3734  sbcimdv  3878  ssel  4002  sscon  4166  uniss  4939  trel3  5293  ssopab2  5565  coss1  5880  fununi  6653  imadif  6662  fss  6763  ssimaex  7007  ssoprab2  7518  poxp  8169  soxp  8170  poseq  8199  suppofssd  8244  pmss12g  8927  ss2ixp  8968  xpdom2  9133  fisup2g  9537  fisupcl  9538  fiinf2g  9569  inf3lem1  9697  epfrs  9800  cfub  10318  cflm  10319  fin23lem34  10415  isf32lem2  10423  axcc4  10508  domtriomlem  10511  ltexprlem3  11107  nnunb  12549  indstr  12981  qbtwnxr  13262  qsqueeze  13263  xrsupsslem  13369  xrinfmsslem  13370  ioc0  13454  climshftlem  15620  o1rlimmul  15665  ramub2  17061  monmat2matmon  22851  tgcl  22997  neips  23142  ssnei2  23145  tgcnp  23282  cnpnei  23293  cnpco  23296  hauscmplem  23435  hauscmp  23436  llyss  23508  nllyss  23509  lfinun  23554  kgen2ss  23584  txcnpi  23637  txcmplem1  23670  fgss  23902  cnpflf2  24029  fclsss1  24051  fclscf  24054  alexsubALT  24080  cnextcn  24096  tsmsxp  24184  mopni3  24528  psmetutop  24601  tngngp3  24698  iscau4  25332  caussi  25350  ovolgelb  25534  mbfi1flim  25778  ellimc3  25934  lhop1  26073  tgbtwndiff  28532  axcontlem4  29000  clwwlknonwwlknonb  30138  sspmval  30765  shmodsi  31421  atcvat4i  32429  cdj3lem2b  32469  ifeqeqx  32565  acunirnmpt  32677  xrge0infss  32767  crefss  33795  issgon  34087  cvmlift2lem12  35282  satfv1  35331  satfvsucsuc  35333  ss2mcls  35536  btwndiff  35991  seglecgr12im  36074  fnessref  36323  waj-ax  36380  lukshef-ax2  36381  bj-isrvec  37260  icorempo  37317  finxpreclem1  37355  fvineqsneq  37378  pibt2  37383  tan2h  37572  poimirlem31  37611  poimir  37613  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  cvrat4  39400  athgt  39413  ps-2  39435  paddss1  39774  paddss2  39775  cdlemg33b0  40658  cdlemg33a  40663  dihjat1lem  41385  fphpdo  42773  irrapxlem2  42779  pell14qrss1234  42812  pell1qrss14  42824  acongtr  42935  ofoaid1  43320  ofoaid2  43321  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  grumnudlem  44254  ax6e2eq  44528  islptre  45540  limccog  45541  grilcbri2  47828  opnneilv  48588