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  4001  ssrexvOLD  4008  ssdif  4094  ssrin  4192  reupick  4279  disjss1  5064  copsexgw  5430  copsexg  5431  propeqop  5447  po3nr  5539  frss  5580  coss2  5796  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  9634  ac6s  10372  reclem2pr  10936  qbtwnxr  13096  ico0  13288  icoshft  13370  2ffzeq  13546  clsslem  14888  r19.2uz  15256  isprm7  16616  prmdvdsncoprmbd  16635  infpn2  16822  prmgaplem4  16963  fthres2  17838  chndss  18519  ablfacrplem  19977  rnglidlmmgm  21180  psdmul  22079  monmat2matmon  22737  neiss  23022  uptx  23538  txcn  23539  nrmr0reg  23662  cnpflfi  23912  cnextcn  23980  caussi  25222  ovolsslem  25410  tgtrisegint  28475  inagswap  28817  shorth  31270  ac6mapd  32601  mptssALT  32652  uzssico  32762  zarclsint  33880  ordtconnlem1  33932  omsmon  34306  omssubadd  34308  r1filimi  35106  subgrtrl  35165  subgrcycl  35167  acycgrsubgr  35190  mclsax  35601  trisegint  36061  segcon2  36138  opnrebl2  36354  bj-19.42t  36806  poimirlem30  37689  itg2addnclem  37710  itg2addnclem2  37711  fdc1  37785  totbndss  37816  ablo4pnp  37919  keridl  38071  dib2dim  41281  dih2dimbALTN  41283  dvh1dim  41480  mapdpglem2  41711  pell14qrss1234  42888  pell1qrss14  42900  rmxycomplete  42949  lnr2i  43148  fzunt  43487  fzuntd  43488  fzunt1d  43489  fzuntgd  43490  rp-fakeanorass  43545  rfcnnnub  45072  or2expropbi  47064  2ffzoeq  47357  ich2exprop  47501  nnsum4primes4  47819  nnsum4primesprm  47821  nnsum4primesgbe  47823  nnsum4primesle9  47825  opnneir  48937