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  7958  1idpru  7959  uzind  9762  xrlttr  10208  fzen  10458  fz0fzelfz0  10545  hashf1lem2  11302  ccatsymb  11386  fisumss  12178  fprodssdc  12376  zeqzmulgcd  12766  lcmgcdlem  12874  lcmdvds  12876  cncongr2  12901  exprmfct  12936  pceu  13097  infpnlem1  13161  prmlem0  13243  isghm  14099  ringadd2  14416  metrest  15698  bcmono  16265  umgredg  16552  bj-charfunbi  17003  bj-om  17129