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  2659  festino  2668  baroco  2670  moeq3  3686  sbcimdv  3825  ssel  3943  sscon  4109  uniss  4882  trel3  5227  axprlem4  5384  ssopab2  5509  coss1  5822  fununi  6594  imadif  6603  fss  6707  ssimaex  6949  ssoprab2  7460  poxp  8110  soxp  8111  poseq  8140  suppofssd  8185  pmss12g  8845  ss2ixp  8886  xpdom2  9041  fisup2g  9427  fisupcl  9428  fiinf2g  9460  inf3lem1  9588  epfrs  9691  cfub  10209  cflm  10210  fin23lem34  10306  isf32lem2  10314  axcc4  10399  domtriomlem  10402  ltexprlem3  10998  nnunb  12445  indstr  12882  qbtwnxr  13167  qsqueeze  13168  xrsupsslem  13274  xrinfmsslem  13275  ioc0  13360  climshftlem  15547  o1rlimmul  15592  ramub2  16992  monmat2matmon  22718  tgcl  22863  neips  23007  ssnei2  23010  tgcnp  23147  cnpnei  23158  cnpco  23161  hauscmplem  23300  hauscmp  23301  llyss  23373  nllyss  23374  lfinun  23419  kgen2ss  23449  txcnpi  23502  txcmplem1  23535  fgss  23767  cnpflf2  23894  fclsss1  23916  fclscf  23919  alexsubALT  23945  cnextcn  23961  tsmsxp  24049  mopni3  24389  psmetutop  24462  tngngp3  24551  iscau4  25186  caussi  25204  ovolgelb  25388  mbfi1flim  25631  ellimc3  25787  lhop1  25926  tgbtwndiff  28440  axcontlem4  28901  clwwlknonwwlknonb  30042  sspmval  30669  shmodsi  31325  atcvat4i  32333  cdj3lem2b  32373  ifeqeqx  32478  acunirnmpt  32590  xrge0infss  32690  constrextdg2lem  33745  crefss  33846  issgon  34120  cvmlift2lem12  35308  satfv1  35357  satfvsucsuc  35359  ss2mcls  35562  btwndiff  36022  seglecgr12im  36105  fnessref  36352  waj-ax  36409  lukshef-ax2  36410  bj-isrvec  37289  icorempo  37346  finxpreclem1  37384  fvineqsneq  37407  pibt2  37412  tan2h  37613  poimirlem31  37652  poimir  37654  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  cvrat4  39444  athgt  39457  ps-2  39479  paddss1  39818  paddss2  39819  cdlemg33b0  40702  cdlemg33a  40707  dihjat1lem  41429  fphpdo  42812  irrapxlem2  42818  pell14qrss1234  42851  pell1qrss14  42863  acongtr  42974  ofoaid1  43354  ofoaid2  43355  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  grumnudlem  44281  ax6e2eq  44554  modelaxreplem1  44975  islptre  45624  limccog  45625  grilcbri2  48007  opnneilv  48901