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  2447  2ax6elem  2470  mopick2  2632  ssrexf  3996  ssrexvOLD  4003  rabss2  4024  ssdif  4091  ssrin  4189  reupick  4276  disjss1  5062  copsexgw  5428  copsexg  5429  propeqop  5445  po3nr  5537  frss  5578  coss2  5795  ordsssuc2  6399  fununi  6556  dffv2  6917  oprabidw  7377  poseq  8088  extmptsuppeq  8118  onfununi  8261  oaass  8476  ssnnfi  9079  fiint  9211  fiss  9308  wemapsolem  9436  elirrv  9483  tcss  9632  ac6s  10375  reclem2pr  10939  qbtwnxr  13099  ico0  13291  icoshft  13373  2ffzeq  13549  clsslem  14891  r19.2uz  15259  isprm7  16619  prmdvdsncoprmbd  16638  infpn2  16825  prmgaplem4  16966  fthres2  17841  chndss  18522  ablfacrplem  19979  rnglidlmmgm  21182  psdmul  22081  monmat2matmon  22739  neiss  23024  uptx  23540  txcn  23541  nrmr0reg  23664  cnpflfi  23914  cnextcn  23982  caussi  25224  ovolsslem  25412  tgtrisegint  28477  inagswap  28819  shorth  31275  ac6mapd  32606  mptssALT  32657  uzssico  32767  zarclsint  33885  ordtconnlem1  33937  omsmon  34311  omssubadd  34313  r1filimi  35114  subgrtrl  35177  subgrcycl  35179  acycgrsubgr  35202  mclsax  35613  trisegint  36072  segcon2  36149  opnrebl2  36365  bj-19.42t  36817  poimirlem30  37689  itg2addnclem  37710  itg2addnclem2  37711  fdc1  37785  totbndss  37816  ablo4pnp  37919  keridl  38071  dib2dim  41341  dih2dimbALTN  41343  dvh1dim  41540  mapdpglem2  41771  pell14qrss1234  42948  pell1qrss14  42960  rmxycomplete  43009  lnr2i  43208  fzunt  43547  fzuntd  43548  fzunt1d  43549  fzuntgd  43550  rp-fakeanorass  43605  rfcnnnub  45132  or2expropbi  47133  2ffzoeq  47426  ich2exprop  47570  nnsum4primes4  47888  nnsum4primesprm  47890  nnsum4primesgbe  47892  nnsum4primesle9  47894  opnneir  49006