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  2445  2ax6elem  2468  mopick2  2630  ssrexf  4013  ssrexvOLD  4020  ssdif  4107  ssrin  4205  reupick  4292  disjss1  5080  copsexgw  5450  copsexg  5451  propeqop  5467  po3nr  5561  frss  5602  coss2  5820  ordsssuc2  6425  fununi  6591  dffv2  6956  oprabidw  7418  poseq  8137  extmptsuppeq  8167  onfununi  8310  oaass  8525  ssnnfi  9133  fiint  9277  fiintOLD  9278  fiss  9375  wemapsolem  9503  tcss  9697  ac6s  10437  reclem2pr  11001  qbtwnxr  13160  ico0  13352  icoshft  13434  2ffzeq  13610  clsslem  14950  r19.2uz  15318  isprm7  16678  prmdvdsncoprmbd  16697  infpn2  16884  prmgaplem4  17025  fthres2  17896  ablfacrplem  19997  rnglidlmmgm  21155  psdmul  22053  monmat2matmon  22711  neiss  22996  uptx  23512  txcn  23513  nrmr0reg  23636  cnpflfi  23886  cnextcn  23954  caussi  25197  ovolsslem  25385  tgtrisegint  28426  inagswap  28768  shorth  31224  ac6mapd  32549  mptssALT  32599  uzssico  32707  zarclsint  33862  ordtconnlem1  33914  omsmon  34289  omssubadd  34291  subgrtrl  35120  subgrcycl  35122  acycgrsubgr  35145  mclsax  35556  trisegint  36016  segcon2  36093  opnrebl2  36309  bj-19.42t  36761  poimirlem30  37644  itg2addnclem  37665  itg2addnclem2  37666  fdc1  37740  totbndss  37771  ablo4pnp  37874  keridl  38026  dib2dim  41237  dih2dimbALTN  41239  dvh1dim  41436  mapdpglem2  41667  pell14qrss1234  42844  pell1qrss14  42856  rmxycomplete  42906  lnr2i  43105  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rp-fakeanorass  43502  rfcnnnub  45030  or2expropbi  47035  2ffzoeq  47328  ich2exprop  47472  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum4primesgbe  47794  nnsum4primesle9  47796  opnneir  48895