Theorem anim1d 612

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 610	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  623  exdistrf  2452  2ax6elem  2475  mopick2  2638  ssrexf  3989  ssrexvOLD  3996  rabss2  4018  ssdif  4085  ssrin  4183  reupick  4270  disjss1  5059  copsexgw  5438  copsexg  5439  propeqop  5455  po3nr  5547  frss  5588  coss2  5805  ordsssuc2  6410  fununi  6567  dffv2  6929  oprabidw  7391  poseq  8101  extmptsuppeq  8131  onfununi  8274  oaass  8489  ssnnfi  9097  fiint  9230  fiss  9330  wemapsolem  9458  elirrv  9505  tcss  9654  ac6s  10397  reclem2pr  10962  qbtwnxr  13143  ico0  13335  icoshft  13417  2ffzeq  13594  clsslem  14937  r19.2uz  15305  isprm7  16669  prmdvdsncoprmbd  16688  infpn2  16875  prmgaplem4  17016  fthres2  17892  chndss  18573  ablfacrplem  20033  rnglidlmmgm  21235  psdmul  22142  monmat2matmon  22799  neiss  23084  uptx  23600  txcn  23601  nrmr0reg  23724  cnpflfi  23974  cnextcn  24042  caussi  25274  ovolsslem  25461  tgtrisegint  28581  inagswap  28923  shorth  31381  ac6mapd  32711  mptssALT  32762  uzssico  32872  zarclsint  34032  ordtconnlem1  34084  omsmon  34458  omssubadd  34460  r1filimi  35262  subgrtrl  35331  subgrcycl  35333  acycgrsubgr  35356  mclsax  35767  trisegint  36226  segcon2  36303  opnrebl2  36519  bj-19.42t  37078  bj-axreprepsep  37398  wl-dfcleq  37844  poimirlem30  37985  itg2addnclem  38006  itg2addnclem2  38007  fdc1  38081  totbndss  38112  ablo4pnp  38215  keridl  38367  dib2dim  41703  dih2dimbALTN  41705  dvh1dim  41902  mapdpglem2  42133  pell14qrss1234  43302  pell1qrss14  43314  rmxycomplete  43363  lnr2i  43562  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  rp-fakeanorass  43958  rfcnnnub  45485  or2expropbi  47494  2ffzoeq  47788  ich2exprop  47943  nnsum4primes4  48277  nnsum4primesprm  48279  nnsum4primesgbe  48281  nnsum4primesle9  48283  opnneir  49394