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  2465  2ax6elem  2489  mopick2  2718  ssrexf  4030  ssrexv  4033  ssdif  4115  ssrin  4209  reupick  4286  disjss1  5029  copsexgw  5373  copsexg  5374  propeqop  5389  po3nr  5482  frss  5516  coss2  5721  ordsssuc2  6273  fununi  6423  dffv2  6750  oprabidw  7181  extmptsuppeq  7848  onfununi  7972  oaass  8181  ssnnfi  8731  fiint  8789  fiss  8882  wemapsolem  9008  tcss  9180  ac6s  9900  reclem2pr  10464  qbtwnxr  12587  ico0  12778  icoshft  12853  2ffzeq  13022  clsslem  14338  r19.2uz  14705  isprm7  16046  infpn2  16243  prmgaplem4  16384  fthres2  17196  ablfacrplem  19181  monmat2matmon  21426  neiss  21711  uptx  22227  txcn  22228  nrmr0reg  22351  cnpflfi  22601  cnextcn  22669  caussi  23894  ovolsslem  24079  tgtrisegint  26279  inagswap  26621  shorth  29066  mptssALT  30414  uzssico  30501  ordtconnlem1  31162  omsmon  31551  omssubadd  31553  subgrtrl  32375  subgrcycl  32377  acycgrsubgr  32400  mclsax  32811  poseq  33090  trisegint  33484  segcon2  33561  opnrebl2  33664  bj-19.42t  34097  poimirlem30  34916  itg2addnclem  34937  itg2addnclem2  34938  fdc1  35015  totbndss  35049  ablo4pnp  35152  keridl  35304  dib2dim  38373  dih2dimbALTN  38375  dvh1dim  38572  mapdpglem2  38803  pell14qrss1234  39446  pell1qrss14  39458  rmxycomplete  39507  lnr2i  39709  rp-fakeanorass  39872  rfcnnnub  41286  or2expropbi  43263  2ffzoeq  43522  ich2exprop  43627  nnsum4primes4  43948  nnsum4primesprm  43950  nnsum4primesgbe  43952  nnsum4primesle9  43954