Theorem anim1d 622

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	anim12d 620	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm3.45  633  exdistrf  2481  2ax6elem  2504  mopick2  2667  ssrexf  4006  rabss2  4033  ssdif  4100  ssrin  4196  reupick  4284  disjss1  5078  copsexgwOLD  5464  copsexg  5465  propeqop  5481  po3nr  5575  frss  5616  coss2  5833  ordsssuc2  6443  fununi  6600  dffv2  6966  oprabidw  7431  poseq  8142  extmptsuppeq  8172  onfununi  8316  oaass  8534  ssnnfi  9142  fiint  9274  fiss  9372  wemapsolem  9500  elirrvOLD  9548  tcss  9699  ac6s  10456  reclem2pr  11021  qbtwnxr  13217  ico0  13409  icoshft  13491  2ffzeq  13668  clsslem  15011  r19.2uz  15393  isprm7  16757  prmdvdsncoprmbd  16776  infpn2  16963  prmgaplem4  17104  fthres2  17981  chndss  18662  ablfacrplem  20128  rnglidlmmgm  21344  psdmul  22289  monmat2matmon  22942  neiss  23227  uptx  23743  txcn  23744  nrmr0reg  23867  cnpflfi  24117  cnextcn  24185  caussi  25417  ovolsslem  25604  tgtrisegint  28726  inagswap  29093  shorth  31556  ac6mapd  32880  mptssALT  32931  uzssico  33041  zarclsint  34179  ordtconnlem1  34231  omsmon  34605  omssubadd  34607  r1filimi  35411  subgrtrl  35496  subgrcycl  35498  acycgrsubgr  35521  mclsax  35932  trisegint  36391  segcon2  36468  opnrebl2  36694  bj-19.42t  37252  bj-axreprepsep  37572  wl-dfcleq  38020  poimirlem30  38161  itg2addnclem  38182  itg2addnclem2  38183  fdc1  38257  totbndss  38288  ablo4pnp  38391  keridl  38543  dib2dim  41879  dih2dimbALTN  41881  dvh1dim  42078  mapdpglem2  42309  pell14qrss1234  43445  pell1qrss14  43457  rmxycomplete  43506  lnr2i  43705  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  rp-fakeanorass  44101  rfcnnnub  45614  or2expropbi  47626  2ffzoeq  47920  ich2exprop  48075  nnsum4primes4  48409  nnsum4primesprm  48411  nnsum4primesgbe  48413  nnsum4primesle9  48415  opnneir  49536