Theorem anim1d 610

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 608	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  621  exdistrf  2455  2ax6elem  2478  mopick2  2640  ssrexf  4075  ssrexvOLD  4082  ssdif  4167  ssrin  4263  reupick  4348  disjss1  5139  copsexgw  5510  copsexg  5511  propeqop  5526  po3nr  5623  frss  5664  coss2  5881  ordsssuc2  6486  fununi  6653  dffv2  7017  oprabidw  7479  poseq  8199  extmptsuppeq  8229  onfununi  8397  oaass  8617  ssnnfi  9235  ssnnfiOLD  9236  fiint  9394  fiintOLD  9395  fiss  9493  wemapsolem  9619  tcss  9813  ac6s  10553  reclem2pr  11117  qbtwnxr  13262  ico0  13453  icoshft  13533  2ffzeq  13706  clsslem  15033  r19.2uz  15400  isprm7  16755  prmdvdsncoprmbd  16774  infpn2  16960  prmgaplem4  17101  fthres2  17999  ablfacrplem  20109  rnglidlmmgm  21278  psdmul  22193  monmat2matmon  22851  neiss  23138  uptx  23654  txcn  23655  nrmr0reg  23778  cnpflfi  24028  cnextcn  24096  caussi  25350  ovolsslem  25538  tgtrisegint  28525  inagswap  28867  shorth  31327  mptssALT  32693  uzssico  32789  zarclsint  33818  ordtconnlem1  33870  omsmon  34263  omssubadd  34265  subgrtrl  35101  subgrcycl  35103  acycgrsubgr  35126  mclsax  35537  trisegint  35992  segcon2  36069  opnrebl2  36287  bj-19.42t  36739  poimirlem30  37610  itg2addnclem  37631  itg2addnclem2  37632  fdc1  37706  totbndss  37737  ablo4pnp  37840  keridl  37992  dib2dim  41200  dih2dimbALTN  41202  dvh1dim  41399  mapdpglem2  41630  pell14qrss1234  42812  pell1qrss14  42824  rmxycomplete  42874  lnr2i  43073  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  rp-fakeanorass  43475  rfcnnnub  44936  or2expropbi  46949  2ffzoeq  47242  ich2exprop  47345  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum4primesgbe  47667  nnsum4primesle9  47669  opnneir  48586