Theorem anim2d 613

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 610	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  2666  festino  2675  baroco  2677  moeq3  3672  sbcimdv  3811  ssel  3929  sscon  4097  uniss  4873  trel3  5216  axprlem4  5373  ssopab2  5502  coss1  5812  fununi  6575  imadif  6584  fss  6686  ssimaex  6927  ssoprab2  7436  poxp  8080  soxp  8081  poseq  8110  suppofssd  8155  pmss12g  8819  ss2ixp  8860  xpdom2  9012  fisup2g  9384  fisupcl  9385  fiinf2g  9417  elirrv  9514  inf3lem1  9549  epfrs  9652  cfub  10171  cflm  10172  fin23lem34  10268  isf32lem2  10276  axcc4  10361  domtriomlem  10364  ltexprlem3  10961  nnunb  12409  indstr  12841  qbtwnxr  13127  qsqueeze  13128  xrsupsslem  13234  xrinfmsslem  13235  ioc0  13320  climshftlem  15509  o1rlimmul  15554  ramub2  16954  chnrss  18550  monmat2matmon  22780  tgcl  22925  neips  23069  ssnei2  23072  tgcnp  23209  cnpnei  23220  cnpco  23223  hauscmplem  23362  hauscmp  23363  llyss  23435  nllyss  23436  lfinun  23481  kgen2ss  23511  txcnpi  23564  txcmplem1  23597  fgss  23829  cnpflf2  23956  fclsss1  23978  fclscf  23981  alexsubALT  24007  cnextcn  24023  tsmsxp  24111  mopni3  24450  psmetutop  24523  tngngp3  24612  iscau4  25247  caussi  25265  ovolgelb  25449  mbfi1flim  25692  ellimc3  25848  lhop1  25987  tgbtwndiff  28590  axcontlem4  29052  clwwlknonwwlknonb  30193  sspmval  30820  shmodsi  31476  atcvat4i  32484  cdj3lem2b  32524  ifeqeqx  32628  acunirnmpt  32748  xrge0infss  32850  constrextdg2lem  33925  crefss  34026  issgon  34300  r1omhfb  35287  r1omhfbregs  35312  cvmlift2lem12  35527  satfv1  35576  satfvsucsuc  35578  ss2mcls  35781  btwndiff  36240  seglecgr12im  36323  fnessref  36570  waj-ax  36627  lukshef-ax2  36628  bj-isrvec  37538  icorempo  37595  finxpreclem1  37633  fvineqsneq  37656  pibt2  37661  tan2h  37852  poimirlem31  37891  poimir  37893  mblfinlem3  37899  mblfinlem4  37900  ismblfin  37901  cvrat4  39808  athgt  39821  ps-2  39843  paddss1  40182  paddss2  40183  cdlemg33b0  41066  cdlemg33a  41071  dihjat1lem  41793  fphpdo  43163  irrapxlem2  43169  pell14qrss1234  43202  pell1qrss14  43214  acongtr  43324  ofoaid1  43704  ofoaid2  43705  fzunt  43800  fzuntd  43801  fzunt1d  43802  fzuntgd  43803  grumnudlem  44630  ax6e2eq  44902  modelaxreplem1  45323  islptre  45968  limccog  45969  grilcbri2  48360  opnneilv  49257