Theorem anim1d 612

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm3.45  623  exdistrf  2469  2ax6elem  2493  mopick2  2722  ssrexf  4033  ssrexv  4036  ssdif  4118  ssrin  4212  reupick  4289  disjss1  5039  copsexgw  5383  copsexg  5384  propeqop  5399  po3nr  5490  frss  5524  coss2  5729  ordsssuc2  6281  fununi  6431  dffv2  6758  oprabidw  7189  extmptsuppeq  7856  onfununi  7980  oaass  8189  ssnnfi  8739  fiint  8797  fiss  8890  wemapsolem  9016  tcss  9188  ac6s  9908  reclem2pr  10472  qbtwnxr  12596  ico0  12787  icoshft  12862  2ffzeq  13031  clsslem  14346  r19.2uz  14713  isprm7  16054  infpn2  16251  prmgaplem4  16392  fthres2  17204  ablfacrplem  19189  monmat2matmon  21434  neiss  21719  uptx  22235  txcn  22236  nrmr0reg  22359  cnpflfi  22609  cnextcn  22677  caussi  23902  ovolsslem  24087  tgtrisegint  26287  inagswap  26629  shorth  29074  mptssALT  30422  uzssico  30509  ordtconnlem1  31169  omsmon  31558  omssubadd  31560  subgrtrl  32382  subgrcycl  32384  acycgrsubgr  32407  mclsax  32818  poseq  33097  trisegint  33491  segcon2  33568  opnrebl2  33671  bj-19.42t  34104  poimirlem30  34924  itg2addnclem  34945  itg2addnclem2  34946  fdc1  35023  totbndss  35057  ablo4pnp  35160  keridl  35312  dib2dim  38381  dih2dimbALTN  38383  dvh1dim  38580  mapdpglem2  38811  pell14qrss1234  39460  pell1qrss14  39472  rmxycomplete  39521  lnr2i  39723  rp-fakeanorass  39886  rfcnnnub  41300  or2expropbi  43276  2ffzoeq  43535  ich2exprop  43640  nnsum4primes4  43961  nnsum4primesprm  43963  nnsum4primesgbe  43965  nnsum4primesle9  43967