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 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is referenced by:  syldan  282  jaoa  722  prlem1  976  equveli  1783  elssabg  4200  suctr  4476  fvun1  5658  opabbrex  6002  poxp  6331  tposfo2  6366  1idprl  7723  1idpru  7724  uzind  9504  xrlttr  9937  fzen  10185  fz0fzelfz0  10269  ccatsymb  11081  fisumss  11778  fprodssdc  11976  zeqzmulgcd  12366  lcmgcdlem  12474  lcmdvds  12476  cncongr2  12501  exprmfct  12535  pceu  12693  infpnlem1  12757  isghm  13654  ringadd2  13864  metrest  15053  bj-charfunbi  15885  bj-om  16011