Theorem 3adant3r3 846

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
3exp.1	⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Assertion

Ref	Expression
3adant3r3	⊢ ((φ ⋀ (ψ ⋀ χ ⋀ τ)) → θ)

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((φ ⋀ ψ ⋀ χ) → θ)
2	1	3expb 836	. 2 ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)
3	2	3adantr3 810	1 ⊢ ((φ ⋀ (ψ ⋀ χ ⋀ τ)) → θ)

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 777

This theorem is referenced by:  grpmuldivass 8084  grppnpcan2 8088  grpnpncan 8090  ablmuldiv 8103  abldivdiv4 8105  nvadd12 8238  nvmdi 8266  nvsubadd 8271  nvmtri2 8296  ipdi 8499  ipsubdir 8504  ipsubdi 8505  homgrf 10701

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain