Theorem anim2d 623

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 620	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  darii  2691  festino  2700  baroco  2702  moeq3  3674  sbcimdv  3811  ssel  3930  sscon  4096  uniss  4879  trel3  5226  axprlem4  5396  ssopab2  5530  coss1  5840  fununi  6611  imadif  6620  fss  6722  ssimaex  6966  ssoprab2  7480  poxp  8122  soxp  8123  poseq  8152  suppofssd  8197  pmss12g  8865  ss2ixp  8906  xpdom2  9058  fisup2g  9427  fisupcl  9428  fiinf2g  9460  elirrvOLD  9558  inf3lem1  9595  epfrs  9698  cfub  10238  cflm  10239  fin23lem34  10336  isf32lem2  10344  axcc4  10429  domtriomlem  10432  ltexprlem3  11029  nnunb  12506  indstr  12946  qbtwnxr  13232  qsqueeze  13233  xrsupsslem  13339  xrinfmsslem  13340  ioc0  13425  climshftlem  15632  o1rlimmul  15677  ramub2  17080  chnrss  18677  monmat2matmon  22992  tgcl  23137  neips  23281  ssnei2  23284  tgcnp  23421  cnpnei  23432  cnpco  23435  hauscmplem  23574  hauscmp  23575  llyss  23647  nllyss  23648  lfinun  23693  kgen2ss  23723  txcnpi  23776  txcmplem1  23809  fgss  24041  cnpflf2  24168  fclsss1  24190  fclscf  24193  alexsubALT  24219  cnextcn  24235  tsmsxp  24323  mopni3  24662  psmetutop  24735  tngngp3  24824  iscau4  25449  caussi  25467  ovolgelb  25650  mbfi1flim  25893  ellimc3  26049  lhop1  26184  tgbtwndiff  28786  axcontlem4  29328  clwwlknonwwlknonb  30468  sspmval  31096  shmodsi  31752  atcvat4i  32760  cdj3lem2b  32800  ifeqeqx  32899  acunirnmpt  33015  xrge0infss  33116  constrextdg2lem  34147  crefss  34248  issgon  34522  r1omhfb  35517  r1omhfbregs  35558  cvmlift2lem12  35814  satfv1  35863  satfvsucsuc  35865  ss2mcls  36068  btwndiff  36527  seglecgr12im  36610  fnessref  36896  waj-ax  36953  lukshef-ax2  36954  bj-isrvec  37966  icorempo  38025  finxpreclem1  38063  fvineqsneq  38086  pibt2  38091  wl-dfcleq  38188  tan2h  38291  poimirlem31  38330  poimir  38332  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  cvrat4  40245  athgt  40258  ps-2  40280  paddss1  40619  paddss2  40620  cdlemg33b0  41503  cdlemg33a  41508  dihjat1lem  42230  fphpdo  43572  irrapxlem2  43578  pell14qrss1234  43611  pell1qrss14  43623  acongtr  43733  ofoaid1  44113  ofoaid2  44114  fzunt  44209  fzuntd  44210  fzunt1d  44211  fzuntgd  44212  grumnudlem  45023  ax6e2eq  45294  modelaxreplem1  45715  islptre  46363  limccog  46364  grilcbri2  48804  opnneilv  49715