Theorem anim1d 610

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 608	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 206  df-an 396

This theorem is referenced by:  pm3.45  621  exdistrf  2447  2ax6elem  2470  mopick2  2639  ssrexf  3981  ssrexv  3984  ssdif  4070  ssrin  4164  reupick  4249  disjss1  5041  copsexgw  5398  copsexg  5399  propeqop  5415  po3nr  5509  frss  5547  coss2  5754  ordsssuc2  6339  fununi  6493  dffv2  6845  oprabidw  7286  extmptsuppeq  7975  onfununi  8143  oaass  8354  ssnnfi  8914  ssnnfiOLD  8915  fiint  9021  fiss  9113  wemapsolem  9239  tcss  9433  ac6s  10171  reclem2pr  10735  qbtwnxr  12863  ico0  13054  icoshft  13134  2ffzeq  13306  clsslem  14623  r19.2uz  14991  isprm7  16341  prmdvdsncoprmbd  16359  infpn2  16542  prmgaplem4  16683  fthres2  17564  ablfacrplem  19583  monmat2matmon  21881  neiss  22168  uptx  22684  txcn  22685  nrmr0reg  22808  cnpflfi  23058  cnextcn  23126  caussi  24366  ovolsslem  24553  tgtrisegint  26764  inagswap  27106  shorth  29558  mptssALT  30914  uzssico  31007  zarclsint  31724  ordtconnlem1  31776  omsmon  32165  omssubadd  32167  subgrtrl  32995  subgrcycl  32997  acycgrsubgr  33020  mclsax  33431  poseq  33729  trisegint  34257  segcon2  34334  opnrebl2  34437  bj-19.42t  34882  poimirlem30  35734  itg2addnclem  35755  itg2addnclem2  35756  fdc1  35831  totbndss  35862  ablo4pnp  35965  keridl  36117  dib2dim  39184  dih2dimbALTN  39186  dvh1dim  39383  mapdpglem2  39614  pell14qrss1234  40594  pell1qrss14  40606  rmxycomplete  40655  lnr2i  40857  rp-fakeanorass  41018  rfcnnnub  42468  or2expropbi  44415  2ffzoeq  44708  ich2exprop  44811  nnsum4primes4  45129  nnsum4primesprm  45131  nnsum4primesgbe  45133  nnsum4primesle9  45135  opnneir  46088