Theorem adantrd 277

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 108	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  syldan  280  jaoa  710  prlem1  958  equveli  1739  elssabg  4109  suctr  4381  fvun1  5533  opabbrex  5862  poxp  6176  tposfo2  6211  1idprl  7504  1idpru  7505  uzind  9269  xrlttr  9695  fzen  9938  fz0fzelfz0  10019  fisumss  11282  fprodssdc  11480  zeqzmulgcd  11845  lcmgcdlem  11945  lcmdvds  11947  cncongr2  11972  exprmfct  12005  metrest  12877  bj-charfunbi  13357  bj-om  13483