Theorem anim2d 589

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  moeq3  3383  ssel  3597  sscon  3744  uniss  4458  trel3  4760  ssopab2  5001  coss1  5277  fununi  5964  imadif  5973  fss  6056  ssimaex  6263  ssoprab2  6711  poxp  7289  soxp  7290  pmss12g  7884  ss2ixp  7921  xpdom2  8055  fisup2g  8374  fisupcl  8375  fiinf2g  8406  inf3lem1  8525  epfrs  8607  cfub  9071  cflm  9072  fin23lem34  9168  isf32lem2  9176  axcc4  9261  domtriomlem  9264  ltexprlem3  9860  nnunb  11288  indstr  11756  qbtwnxr  12031  qsqueeze  12032  xrsupsslem  12137  xrinfmsslem  12138  ioc0  12222  climshftlem  14305  o1rlimmul  14349  ramub2  15718  monmat2matmon  20629  tgcl  20773  neips  20917  ssnei2  20920  tgcnp  21057  cnpnei  21068  cnpco  21071  hauscmplem  21209  hauscmp  21210  llyss  21282  nllyss  21283  lfinun  21328  kgen2ss  21358  txcnpi  21411  txcmplem1  21444  fgss  21677  cnpflf2  21804  fclsss1  21826  fclscf  21829  alexsubALT  21855  cnextcn  21871  tsmsxp  21958  mopni3  22299  psmetutop  22372  tngngp3  22460  iscau4  23077  caussi  23095  ovolgelb  23248  mbfi1flim  23490  ellimc3  23643  lhop1  23777  tgbtwndiff  25401  axcontlem4  25847  sspmval  27588  shmodsi  28248  atcvat4i  29256  cdj3lem2b  29296  ifeqeqx  29361  acunirnmpt  29459  xrge0infss  29525  crefss  29916  issgon  30186  cvmlift2lem12  31296  ss2mcls  31465  poseq  31750  btwndiff  32134  seglecgr12im  32217  fnessref  32352  waj-ax  32413  lukshef-ax2  32414  icorempt2  33199  finxpreclem1  33226  tan2h  33401  poimirlem31  33440  poimir  33442  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  cvrat4  34729  athgt  34742  ps-2  34764  paddss1  35103  paddss2  35104  cdlemg33b0  35989  cdlemg33a  35994  dihjat1lem  36717  fphpdo  37381  irrapxlem2  37387  pell14qrss1234  37420  pell1qrss14  37432  acongtr  37545  ax6e2eq  38773  islptre  39851  limccog  39852