Theorem anim1d 611

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  pm3.45  622  exdistrf  2448  2ax6elem  2471  mopick2  2640  ssrexf  3986  ssrexv  3989  ssdif  4075  ssrin  4168  reupick  4253  disjss1  5046  copsexgw  5405  copsexg  5406  propeqop  5422  po3nr  5519  frss  5557  coss2  5768  ordsssuc2  6358  fununi  6516  dffv2  6872  oprabidw  7315  extmptsuppeq  8013  onfununi  8181  oaass  8401  ssnnfi  8961  ssnnfiOLD  8962  fiint  9100  fiss  9192  wemapsolem  9318  tcss  9511  ac6s  10249  reclem2pr  10813  qbtwnxr  12943  ico0  13134  icoshft  13214  2ffzeq  13386  clsslem  14704  r19.2uz  15072  isprm7  16422  prmdvdsncoprmbd  16440  infpn2  16623  prmgaplem4  16764  fthres2  17657  ablfacrplem  19677  monmat2matmon  21982  neiss  22269  uptx  22785  txcn  22786  nrmr0reg  22909  cnpflfi  23159  cnextcn  23227  caussi  24470  ovolsslem  24657  tgtrisegint  26869  inagswap  27211  shorth  29666  mptssALT  31021  uzssico  31114  zarclsint  31831  ordtconnlem1  31883  omsmon  32274  omssubadd  32276  subgrtrl  33104  subgrcycl  33106  acycgrsubgr  33129  mclsax  33540  poseq  33811  trisegint  34339  segcon2  34416  opnrebl2  34519  bj-19.42t  34964  poimirlem30  35816  itg2addnclem  35837  itg2addnclem2  35838  fdc1  35913  totbndss  35944  ablo4pnp  36047  keridl  36199  dib2dim  39264  dih2dimbALTN  39266  dvh1dim  39463  mapdpglem2  39694  pell14qrss1234  40685  pell1qrss14  40697  rmxycomplete  40746  lnr2i  40948  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  rp-fakeanorass  41127  rfcnnnub  42586  or2expropbi  44539  2ffzoeq  44831  ich2exprop  44934  nnsum4primes4  45252  nnsum4primesprm  45254  nnsum4primesgbe  45256  nnsum4primesle9  45258  opnneir  46211