Theorem anim1d 612

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)

Hypothesis

Ref	Expression
anim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
anim1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Proof of Theorem anim1d

Step	Hyp	Ref	Expression
1		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 24	. 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:  pm3.45  623  exdistrf  2451  2ax6elem  2474  mopick2  2637  ssrexf  3988  ssrexvOLD  3995  rabss2  4017  ssdif  4084  ssrin  4182  reupick  4269  disjss1  5058  copsexgwOLD  5444  copsexg  5445  propeqop  5461  po3nr  5554  frss  5595  coss2  5811  ordsssuc2  6416  fununi  6573  dffv2  6935  oprabidw  7398  poseq  8108  extmptsuppeq  8138  onfununi  8281  oaass  8496  ssnnfi  9104  fiint  9237  fiss  9337  wemapsolem  9465  elirrv  9512  tcss  9663  ac6s  10406  reclem2pr  10971  qbtwnxr  13152  ico0  13344  icoshft  13426  2ffzeq  13603  clsslem  14946  r19.2uz  15314  isprm7  16678  prmdvdsncoprmbd  16697  infpn2  16884  prmgaplem4  17025  fthres2  17901  chndss  18582  ablfacrplem  20042  rnglidlmmgm  21243  psdmul  22132  monmat2matmon  22789  neiss  23074  uptx  23590  txcn  23591  nrmr0reg  23714  cnpflfi  23964  cnextcn  24032  caussi  25264  ovolsslem  25451  tgtrisegint  28567  inagswap  28909  shorth  31366  ac6mapd  32696  mptssALT  32747  uzssico  32857  zarclsint  34016  ordtconnlem1  34068  omsmon  34442  omssubadd  34444  r1filimi  35246  subgrtrl  35315  subgrcycl  35317  acycgrsubgr  35340  mclsax  35751  trisegint  36210  segcon2  36287  opnrebl2  36503  bj-19.42t  37062  bj-axreprepsep  37382  wl-dfcleq  37830  poimirlem30  37971  itg2addnclem  37992  itg2addnclem2  37993  fdc1  38067  totbndss  38098  ablo4pnp  38201  keridl  38353  dib2dim  41689  dih2dimbALTN  41691  dvh1dim  41888  mapdpglem2  42119  pell14qrss1234  43284  pell1qrss14  43296  rmxycomplete  43345  lnr2i  43544  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  rp-fakeanorass  43940  rfcnnnub  45467  or2expropbi  47482  2ffzoeq  47776  ich2exprop  47931  nnsum4primes4  48265  nnsum4primesprm  48267  nnsum4primesgbe  48269  nnsum4primesle9  48271  opnneir  49382