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  2665  festino  2674  baroco  2676  moeq3  3700  sbcimdv  3839  ssel  3957  sscon  4123  uniss  4896  trel3  5244  axprlem4  5401  ssopab2  5526  coss1  5840  fununi  6616  imadif  6625  fss  6727  ssimaex  6969  ssoprab2  7480  poxp  8132  soxp  8133  poseq  8162  suppofssd  8207  pmss12g  8888  ss2ixp  8929  xpdom2  9086  fisup2g  9486  fisupcl  9487  fiinf2g  9519  inf3lem1  9647  epfrs  9750  cfub  10268  cflm  10269  fin23lem34  10365  isf32lem2  10373  axcc4  10458  domtriomlem  10461  ltexprlem3  11057  nnunb  12502  indstr  12937  qbtwnxr  13221  qsqueeze  13222  xrsupsslem  13328  xrinfmsslem  13329  ioc0  13414  climshftlem  15595  o1rlimmul  15640  ramub2  17039  monmat2matmon  22767  tgcl  22912  neips  23056  ssnei2  23059  tgcnp  23196  cnpnei  23207  cnpco  23210  hauscmplem  23349  hauscmp  23350  llyss  23422  nllyss  23423  lfinun  23468  kgen2ss  23498  txcnpi  23551  txcmplem1  23584  fgss  23816  cnpflf2  23943  fclsss1  23965  fclscf  23968  alexsubALT  23994  cnextcn  24010  tsmsxp  24098  mopni3  24438  psmetutop  24511  tngngp3  24600  iscau4  25236  caussi  25254  ovolgelb  25438  mbfi1flim  25681  ellimc3  25837  lhop1  25976  tgbtwndiff  28490  axcontlem4  28951  clwwlknonwwlknonb  30092  sspmval  30719  shmodsi  31375  atcvat4i  32383  cdj3lem2b  32423  ifeqeqx  32528  acunirnmpt  32642  xrge0infss  32742  constrextdg2lem  33787  crefss  33885  issgon  34159  cvmlift2lem12  35341  satfv1  35390  satfvsucsuc  35392  ss2mcls  35595  btwndiff  36050  seglecgr12im  36133  fnessref  36380  waj-ax  36437  lukshef-ax2  36438  bj-isrvec  37317  icorempo  37374  finxpreclem1  37412  fvineqsneq  37435  pibt2  37440  tan2h  37641  poimirlem31  37680  poimir  37682  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  cvrat4  39467  athgt  39480  ps-2  39502  paddss1  39841  paddss2  39842  cdlemg33b0  40725  cdlemg33a  40730  dihjat1lem  41452  fphpdo  42807  irrapxlem2  42813  pell14qrss1234  42846  pell1qrss14  42858  acongtr  42969  ofoaid1  43349  ofoaid2  43350  fzunt  43446  fzuntd  43447  fzunt1d  43448  fzuntgd  43449  grumnudlem  44276  ax6e2eq  44549  modelaxreplem1  44970  islptre  45615  limccog  45616  grilcbri2  47983  opnneilv  48850