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  2452  2ax6elem  2475  mopick2  2638  ssrexf  4002  ssrexvOLD  4009  rabss2  4031  ssdif  4098  ssrin  4196  reupick  4283  disjss1  5073  copsexgw  5446  copsexg  5447  propeqop  5463  po3nr  5555  frss  5596  coss2  5813  ordsssuc2  6418  fununi  6575  dffv2  6937  oprabidw  7399  poseq  8110  extmptsuppeq  8140  onfununi  8283  oaass  8498  ssnnfi  9106  fiint  9239  fiss  9339  wemapsolem  9467  elirrv  9514  tcss  9663  ac6s  10406  reclem2pr  10971  qbtwnxr  13127  ico0  13319  icoshft  13401  2ffzeq  13577  clsslem  14919  r19.2uz  15287  isprm7  16647  prmdvdsncoprmbd  16666  infpn2  16853  prmgaplem4  16994  fthres2  17870  chndss  18551  ablfacrplem  20008  rnglidlmmgm  21212  psdmul  22121  monmat2matmon  22780  neiss  23065  uptx  23581  txcn  23582  nrmr0reg  23705  cnpflfi  23955  cnextcn  24023  caussi  25265  ovolsslem  25453  tgtrisegint  28583  inagswap  28925  shorth  31382  ac6mapd  32712  mptssALT  32763  uzssico  32874  zarclsint  34049  ordtconnlem1  34101  omsmon  34475  omssubadd  34477  r1filimi  35278  subgrtrl  35346  subgrcycl  35348  acycgrsubgr  35371  mclsax  35782  trisegint  36241  segcon2  36318  opnrebl2  36534  bj-19.42t  37002  bj-axreprepsep  37317  poimirlem30  37895  itg2addnclem  37916  itg2addnclem2  37917  fdc1  37991  totbndss  38022  ablo4pnp  38125  keridl  38277  dib2dim  41613  dih2dimbALTN  41615  dvh1dim  41812  mapdpglem2  42043  pell14qrss1234  43207  pell1qrss14  43219  rmxycomplete  43268  lnr2i  43467  fzunt  43805  fzuntd  43806  fzunt1d  43807  fzuntgd  43808  rp-fakeanorass  43863  rfcnnnub  45390  or2expropbi  47388  2ffzoeq  47681  ich2exprop  47825  nnsum4primes4  48143  nnsum4primesprm  48145  nnsum4primesgbe  48147  nnsum4primesle9  48149  opnneir  49260