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  2445  2ax6elem  2468  mopick2  2630  ssrexf  4004  ssrexvOLD  4011  ssdif  4097  ssrin  4195  reupick  4282  disjss1  5068  copsexgw  5437  copsexg  5438  propeqop  5454  po3nr  5546  frss  5587  coss2  5803  ordsssuc2  6404  fununi  6561  dffv2  6922  oprabidw  7384  poseq  8098  extmptsuppeq  8128  onfununi  8271  oaass  8486  ssnnfi  9093  fiint  9235  fiintOLD  9236  fiss  9333  wemapsolem  9461  elirrv  9508  tcss  9659  ac6s  10397  reclem2pr  10961  qbtwnxr  13120  ico0  13312  icoshft  13394  2ffzeq  13570  clsslem  14909  r19.2uz  15277  isprm7  16637  prmdvdsncoprmbd  16656  infpn2  16843  prmgaplem4  16984  fthres2  17859  ablfacrplem  19964  rnglidlmmgm  21170  psdmul  22069  monmat2matmon  22727  neiss  23012  uptx  23528  txcn  23529  nrmr0reg  23652  cnpflfi  23902  cnextcn  23970  caussi  25213  ovolsslem  25401  tgtrisegint  28462  inagswap  28804  shorth  31257  ac6mapd  32582  mptssALT  32632  uzssico  32740  zarclsint  33838  ordtconnlem1  33890  omsmon  34265  omssubadd  34267  subgrtrl  35105  subgrcycl  35107  acycgrsubgr  35130  mclsax  35541  trisegint  36001  segcon2  36078  opnrebl2  36294  bj-19.42t  36746  poimirlem30  37629  itg2addnclem  37650  itg2addnclem2  37651  fdc1  37725  totbndss  37756  ablo4pnp  37859  keridl  38011  dib2dim  41222  dih2dimbALTN  41224  dvh1dim  41421  mapdpglem2  41652  pell14qrss1234  42829  pell1qrss14  42841  rmxycomplete  42890  lnr2i  43089  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  rp-fakeanorass  43486  rfcnnnub  45014  or2expropbi  47019  2ffzoeq  47312  ich2exprop  47456  nnsum4primes4  47774  nnsum4primesprm  47776  nnsum4primesgbe  47778  nnsum4primesle9  47780  opnneir  48892