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

This theorem is referenced by:  darii  2660  festino  2669  baroco  2671  moeq3  3707  sbcimdv  3850  ssel  3974  sselOLD  3975  sscon  4137  uniss  4915  trel3  5274  ssopab2  5545  coss1  5853  fununi  6620  imadif  6629  fss  6731  ssimaex  6973  ssoprab2  7473  poxp  8110  soxp  8111  poseq  8140  suppofssd  8184  pmss12g  8859  ss2ixp  8900  xpdom2  9063  fisup2g  9459  fisupcl  9460  fiinf2g  9491  inf3lem1  9619  epfrs  9722  cfub  10240  cflm  10241  fin23lem34  10337  isf32lem2  10345  axcc4  10430  domtriomlem  10433  ltexprlem3  11029  nnunb  12464  indstr  12896  qbtwnxr  13175  qsqueeze  13176  xrsupsslem  13282  xrinfmsslem  13283  ioc0  13367  climshftlem  15514  o1rlimmul  15559  ramub2  16943  monmat2matmon  22317  tgcl  22463  neips  22608  ssnei2  22611  tgcnp  22748  cnpnei  22759  cnpco  22762  hauscmplem  22901  hauscmp  22902  llyss  22974  nllyss  22975  lfinun  23020  kgen2ss  23050  txcnpi  23103  txcmplem1  23136  fgss  23368  cnpflf2  23495  fclsss1  23517  fclscf  23520  alexsubALT  23546  cnextcn  23562  tsmsxp  23650  mopni3  23994  psmetutop  24067  tngngp3  24164  iscau4  24787  caussi  24805  ovolgelb  24988  mbfi1flim  25232  ellimc3  25387  lhop1  25522  tgbtwndiff  27746  axcontlem4  28214  clwwlknonwwlknonb  29348  sspmval  29973  shmodsi  30629  atcvat4i  31637  cdj3lem2b  31677  ifeqeqx  31761  acunirnmpt  31871  xrge0infss  31960  crefss  32817  issgon  33109  cvmlift2lem12  34293  satfv1  34342  satfvsucsuc  34344  ss2mcls  34547  btwndiff  34987  seglecgr12im  35070  fnessref  35230  waj-ax  35287  lukshef-ax2  35288  bj-isrvec  36163  icorempo  36220  finxpreclem1  36258  fvineqsneq  36281  pibt2  36286  tan2h  36468  poimirlem31  36507  poimir  36509  mblfinlem3  36515  mblfinlem4  36516  ismblfin  36517  cvrat4  38302  athgt  38315  ps-2  38337  paddss1  38676  paddss2  38677  cdlemg33b0  39560  cdlemg33a  39565  dihjat1lem  40287  fphpdo  41540  irrapxlem2  41546  pell14qrss1234  41579  pell1qrss14  41591  acongtr  41702  ofoaid1  42093  ofoaid2  42094  fzunt  42191  fzuntd  42192  fzunt1d  42193  fzuntgd  42194  grumnudlem  43029  ax6e2eq  43303  islptre  44321  limccog  44322  opnneilv  47494