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  727  prlem1  981  equveli  1807  elssabg  4238  suctr  4518  fvun1  5712  opabbrex  6065  poxp  6397  tposfo2  6433  1idprl  7810  1idpru  7811  uzind  9591  xrlttr  10030  fzen  10278  fz0fzelfz0  10362  ccatsymb  11183  fisumss  11958  fprodssdc  12156  zeqzmulgcd  12546  lcmgcdlem  12654  lcmdvds  12656  cncongr2  12681  exprmfct  12715  pceu  12873  infpnlem1  12937  isghm  13835  ringadd2  14046  metrest  15236  umgredg  16002  bj-charfunbi  16432  bj-om  16558