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  721  prlem1  975  equveli  1781  elssabg  4191  suctr  4467  fvun1  5644  opabbrex  5988  poxp  6317  tposfo2  6352  1idprl  7702  1idpru  7703  uzind  9483  xrlttr  9916  fzen  10164  fz0fzelfz0  10248  ccatsymb  11056  fisumss  11674  fprodssdc  11872  zeqzmulgcd  12262  lcmgcdlem  12370  lcmdvds  12372  cncongr2  12397  exprmfct  12431  pceu  12589  infpnlem1  12653  isghm  13550  ringadd2  13760  metrest  14949  bj-charfunbi  15709  bj-om  15835