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  2666  festino  2675  baroco  2677  moeq3  3647  sbcimdv  3790  ssel  3914  sselOLD  3915  sscon  4073  uniss  4847  trel3  5199  ssopab2  5459  coss1  5764  fununi  6509  imadif  6518  fss  6617  ssimaex  6853  ssoprab2  7343  poxp  7969  soxp  7970  suppofssd  8019  pmss12g  8657  ss2ixp  8698  xpdom2  8854  fisup2g  9227  fisupcl  9228  fiinf2g  9259  inf3lem1  9386  epfrs  9489  cfub  10005  cflm  10006  fin23lem34  10102  isf32lem2  10110  axcc4  10195  domtriomlem  10198  ltexprlem3  10794  nnunb  12229  indstr  12656  qbtwnxr  12934  qsqueeze  12935  xrsupsslem  13041  xrinfmsslem  13042  ioc0  13126  climshftlem  15283  o1rlimmul  15328  ramub2  16715  monmat2matmon  21973  tgcl  22119  neips  22264  ssnei2  22267  tgcnp  22404  cnpnei  22415  cnpco  22418  hauscmplem  22557  hauscmp  22558  llyss  22630  nllyss  22631  lfinun  22676  kgen2ss  22706  txcnpi  22759  txcmplem1  22792  fgss  23024  cnpflf2  23151  fclsss1  23173  fclscf  23176  alexsubALT  23202  cnextcn  23218  tsmsxp  23306  mopni3  23650  psmetutop  23723  tngngp3  23820  iscau4  24443  caussi  24461  ovolgelb  24644  mbfi1flim  24888  ellimc3  25043  lhop1  25178  tgbtwndiff  26867  axcontlem4  27335  clwwlknonwwlknonb  28470  sspmval  29095  shmodsi  29751  atcvat4i  30759  cdj3lem2b  30799  ifeqeqx  30885  acunirnmpt  30996  xrge0infss  31083  crefss  31799  issgon  32091  cvmlift2lem12  33276  satfv1  33325  satfvsucsuc  33327  ss2mcls  33530  poseq  33802  btwndiff  34329  seglecgr12im  34412  fnessref  34546  waj-ax  34603  lukshef-ax2  34604  bj-isrvec  35465  icorempo  35522  finxpreclem1  35560  fvineqsneq  35583  pibt2  35588  tan2h  35769  poimirlem31  35808  poimir  35810  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  cvrat4  37457  athgt  37470  ps-2  37492  paddss1  37831  paddss2  37832  cdlemg33b0  38715  cdlemg33a  38720  dihjat1lem  39442  fphpdo  40639  irrapxlem2  40645  pell14qrss1234  40678  pell1qrss14  40690  acongtr  40800  fzunt  41062  fzuntd  41063  fzunt1d  41064  fzuntgd  41065  grumnudlem  41903  ax6e2eq  42177  islptre  43160  limccog  43161  opnneilv  46202