Theorem adantrd 279

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

Ref	Expression
adantrd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
adantrd	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  syldan  282  jaoa  732  prlem1  986  equveli  1812  elssabg  4284  suctr  4566  fvun1  5769  opabbrex  6132  poxp  6468  tposfo2  6538  1idprl  7957  1idpru  7958  uzind  9757  xrlttr  10197  fzen  10447  fz0fzelfz0  10534  hashf1lem2  11286  ccatsymb  11370  fisumss  12159  fprodssdc  12357  zeqzmulgcd  12747  lcmgcdlem  12855  lcmdvds  12857  cncongr2  12882  exprmfct  12916  pceu  13074  infpnlem1  13138  isghm  14046  ringadd2  14332  metrest  15607  umgredg  16386  bj-charfunbi  16837  bj-om  16963