Theorem anim2d 624

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 621	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

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

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 402

This theorem is used by:  darii  2689  festino  2698  baroco  2700  moeq3  3669  sbcimdv  3806  ssel  3924  sscon  4089  uniss  4874  trel3  5220  axprlem4  5387  ssopab2  5517  coss1  5829  fununi  6603  imadif  6612  fss  6714  ssimaex  6958  ssoprab2  7476  poxp  8123  soxp  8124  poseq  8153  suppofssd  8198  pmss12g  8875  ss2ixp  8916  xpdom2  9069  fisup2g  9439  fisupcl  9440  fiinf2g  9472  elirrvOLD  9570  inf3lem1  9607  epfrs  9710  cfub  10298  cflm  10299  fin23lem34  10396  isf32lem2  10404  axcc4  10489  domtriomlem  10492  ltexprlem3  11095  nnunb  12572  indstr  13013  qbtwnxr  13300  qsqueeze  13301  xrsupsslem  13407  xrinfmsslem  13408  ioc0  13493  climshftlem  15709  o1rlimmul  15754  ramub2  17154  chnrss  18751  monmat2matmon  23104  tgcl  23249  neips  23393  ssnei2  23396  tgcnp  23533  cnpnei  23544  cnpco  23547  hauscmplem  23686  hauscmp  23687  llyss  23760  nllyss  23761  lfinun  23806  kgen2ss  23836  txcnpi  23889  txcmplem1  23922  fgss  24154  cnpflf2  24281  fclsss1  24303  fclscf  24306  alexsubALT  24332  cnextcn  24348  tsmsxp  24436  mopni3  24775  psmetutop  24848  tngngp3  24937  iscau4  25562  caussi  25580  ovolgelb  25763  mbfi1flim  26006  ellimc3  26161  lhop1  26296  tgbtwndiff  28903  axcontlem4  29479  clwwlknonwwlknonb  30631  sspmval  31269  shmodsi  31925  atcvat4i  32933  cdj3lem2b  32973  ifeqeqx  33072  acunirnmpt  33187  xrge0infss  33286  constrextdg2lem  34314  crefss  34415  issgon  34689  r1omhfb  35669  r1omhfbregs  35730  cvmlift2lem12  36000  satfv1  36049  satfvsucsuc  36051  ss2mcls  36254  btwndiff  36714  seglecgr12im  36797  fnessref  37067  waj-ax  37124  lukshef-ax2  37125  bj-isrvec  38135  icorempo  38194  finxpreclem1  38232  fvineqsneq  38255  pibt2  38260  wl-dfcleq  38357  tan2h  38455  poimirlem31  38489  poimir  38491  mblfinlem3  38497  mblfinlem4  38498  ismblfin  38499  cvrat4  40420  athgt  40433  ps-2  40455  paddss1  40794  paddss2  40795  cdlemg33b0  41678  cdlemg33a  41683  dihjat1lem  42405  fphpdo  43762  irrapxlem2  43768  pell14qrss1234  43801  pell1qrss14  43813  acongtr  43923  ofoaid1  44303  ofoaid2  44304  fzunt  44399  fzuntd  44400  fzunt1d  44401  fzuntgd  44402  grumnudlem  45213  ax6e2eq  45484  modelaxreplem1  45905  islptre  46553  limccog  46554  grilcbri2  49031  opnneilv  49939