Theorem anim1d 623

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	anim12d 621	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.45  634  exdistrf  2479  2ax6elem  2502  mopick2  2665  ssrexf  3980  rabss2  4005  ssdif  4083  ssrin  4141  reupick  4277  disjss1  5079  copsexgwOLD  5466  copsexg  5467  propeqop  5484  po3nr  5579  frss  5620  coss2  5841  ordsssuc2  6477  fununi  6640  dffv2  7006  oprabidw  7477  poseq  8205  extmptsuppeq  8236  onfununi  8380  oaass  8600  ssnnfi  9216  fiint  9349  fiss  9446  wemapsolem  9574  elirrvOLD  9622  tcss  9773  r1filimi  9933  ac6s  10592  reclem2pr  11163  qbtwnxr  13360  ico0  13552  icoshft  13634  2ffzeq  13813  clsslem  15169  r19.2uz  15551  isprm7  16916  prmdvdsncoprmbd  16935  infpn2  17123  prmgaplem4  17264  fthres2  18141  chndss  18822  ablfacrplem  20314  rnglidlmmgm  21566  psdmul  22520  monmat2matmon  23175  neiss  23460  uptx  23977  txcn  23978  nrmr0reg  24101  cnpflfi  24351  cnextcn  24419  caussi  25651  ovolsslem  25838  fltoprmlem1  28026  tgtrisegint  28995  inagswap  29393  subgrtrl  30327  subgrcycl  30418  shorth  31930  ac6mapd  33292  mptssALT  33342  uzssico  33449  zarclsint  34587  ordtconnlem1  34639  omsmon  35013  omssubadd  35015  jf1  36023  acycgrsubgr  36093  mclsax  36514  trisegint  36984  segcon2  37061  opnrebl2  37300  bj-19.42t  37858  bj-axreprepsep  38195  wl-dfcleq  38642  poimirlem30  38773  itg2addnclem  38794  itg2addnclem2  38795  fdc1  38883  totbndss  38914  ablo4pnp  39017  keridl  39169  dib2dim  42503  dih2dimbALTN  42505  dvh1dim  42702  mapdpglem2  42933  pell14qrss1234  44067  pell1qrss14  44079  rmxycomplete  44128  lnr2i  44321  fzunt  44659  fzuntd  44660  fzunt1d  44661  fzuntgd  44662  rp-fakeanorass  44717  rfcnnnub  46269  or2expropbi  48319  2ffzoeq  48613  ich2exprop  48768  nnsum4primes4  49102  nnsum4primesprm  49104  nnsum4primesgbe  49106  nnsum4primesle9  49108  opnneir  50236