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 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  622  exdistrf  2450  2ax6elem  2473  mopick2  2635  ssrexf  4062  ssrexvOLD  4069  ssdif  4154  ssrin  4250  reupick  4335  disjss1  5121  copsexgw  5501  copsexg  5502  propeqop  5517  po3nr  5612  frss  5653  coss2  5870  ordsssuc2  6477  fununi  6643  dffv2  7004  oprabidw  7462  poseq  8182  extmptsuppeq  8212  onfununi  8380  oaass  8598  ssnnfi  9208  fiint  9364  fiintOLD  9365  fiss  9462  wemapsolem  9588  tcss  9782  ac6s  10522  reclem2pr  11086  qbtwnxr  13239  ico0  13430  icoshft  13510  2ffzeq  13686  clsslem  15020  r19.2uz  15387  isprm7  16742  prmdvdsncoprmbd  16761  infpn2  16947  prmgaplem4  17088  fthres2  17986  ablfacrplem  20100  rnglidlmmgm  21273  psdmul  22188  monmat2matmon  22846  neiss  23133  uptx  23649  txcn  23650  nrmr0reg  23773  cnpflfi  24023  cnextcn  24091  caussi  25345  ovolsslem  25533  tgtrisegint  28522  inagswap  28864  shorth  31324  mptssALT  32692  uzssico  32793  zarclsint  33833  ordtconnlem1  33885  omsmon  34280  omssubadd  34282  subgrtrl  35118  subgrcycl  35120  acycgrsubgr  35143  mclsax  35554  trisegint  36010  segcon2  36087  opnrebl2  36304  bj-19.42t  36756  poimirlem30  37637  itg2addnclem  37658  itg2addnclem2  37659  fdc1  37733  totbndss  37764  ablo4pnp  37867  keridl  38019  dib2dim  41226  dih2dimbALTN  41228  dvh1dim  41425  mapdpglem2  41656  pell14qrss1234  42844  pell1qrss14  42856  rmxycomplete  42906  lnr2i  43105  fzunt  43445  fzuntd  43446  fzunt1d  43447  fzuntgd  43448  rp-fakeanorass  43503  rfcnnnub  44974  or2expropbi  46984  2ffzoeq  47277  ich2exprop  47396  nnsum4primes4  47714  nnsum4primesprm  47716  nnsum4primesgbe  47718  nnsum4primesle9  47720  opnneir  48703