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  6064  poxp  6396  tposfo2  6432  1idprl  7809  1idpru  7810  uzind  9590  xrlttr  10029  fzen  10277  fz0fzelfz0  10361  ccatsymb  11178  fisumss  11952  fprodssdc  12150  zeqzmulgcd  12540  lcmgcdlem  12648  lcmdvds  12650  cncongr2  12675  exprmfct  12709  pceu  12867  infpnlem1  12931  isghm  13829  ringadd2  14039  metrest  15229  umgredg  15995  bj-charfunbi  16406  bj-om  16532