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 206  df-an 396

This theorem is referenced by:  pm3.45  621  exdistrf  2445  2ax6elem  2468  mopick2  2632  ssrexf  4048  ssrexv  4051  ssdif  4139  ssrin  4233  reupick  4318  disjss1  5119  copsexgw  5490  copsexg  5491  propeqop  5507  po3nr  5603  frss  5643  coss2  5856  ordsssuc2  6455  fununi  6623  dffv2  6986  oprabidw  7443  poseq  8149  extmptsuppeq  8178  onfununi  8347  oaass  8567  ssnnfi  9175  ssnnfiOLD  9176  fiint  9330  fiss  9425  wemapsolem  9551  tcss  9745  ac6s  10485  reclem2pr  11049  qbtwnxr  13186  ico0  13377  icoshft  13457  2ffzeq  13629  clsslem  14938  r19.2uz  15305  isprm7  16652  prmdvdsncoprmbd  16670  infpn2  16853  prmgaplem4  16994  fthres2  17892  ablfacrplem  19983  rnglidlmmgm  21123  monmat2matmon  22646  neiss  22933  uptx  23449  txcn  23450  nrmr0reg  23573  cnpflfi  23823  cnextcn  23891  caussi  25145  ovolsslem  25333  tgtrisegint  28183  inagswap  28525  shorth  30981  mptssALT  32333  uzssico  32428  zarclsint  33316  ordtconnlem1  33368  omsmon  33761  omssubadd  33763  subgrtrl  34588  subgrcycl  34590  acycgrsubgr  34613  mclsax  35024  trisegint  35470  segcon2  35547  opnrebl2  35670  bj-19.42t  36115  poimirlem30  36982  itg2addnclem  37003  itg2addnclem2  37004  fdc1  37078  totbndss  37109  ablo4pnp  37212  keridl  37364  dib2dim  40578  dih2dimbALTN  40580  dvh1dim  40777  mapdpglem2  41008  pell14qrss1234  42057  pell1qrss14  42069  rmxycomplete  42119  lnr2i  42321  fzunt  42669  fzuntd  42670  fzunt1d  42671  fzuntgd  42672  rp-fakeanorass  42727  rfcnnnub  44183  or2expropbi  46203  2ffzoeq  46495  ich2exprop  46598  nnsum4primes4  46916  nnsum4primesprm  46918  nnsum4primesgbe  46920  nnsum4primesle9  46922  opnneir  47701