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  728  prlem1  982  equveli  1808  elssabg  4265  suctr  4547  fvun1  5748  opabbrex  6105  poxp  6441  tposfo2  6511  1idprl  7921  1idpru  7922  uzind  9707  xrlttr  10147  fzen  10397  fz0fzelfz0  10483  ccatsymb  11315  fisumss  12103  fprodssdc  12301  zeqzmulgcd  12691  lcmgcdlem  12799  lcmdvds  12801  cncongr2  12826  exprmfct  12860  pceu  13018  infpnlem1  13082  isghm  13996  ringadd2  14270  metrest  15497  umgredg  16266  bj-charfunbi  16707  bj-om  16833