Theorem 3adantl3 807

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl3

Step	Hyp	Ref	Expression
1		3adantl.1	. . . 4 ⊢ (((φ ⋀ ψ) ⋀ χ) → θ)
2	1	ex 373	. . 3 ⊢ ((φ ⋀ ψ) → (χ → θ))
3	2	3adant3 801	. 2 ⊢ ((φ ⋀ ψ ⋀ τ) → (χ → θ))
4	3	imp 350	1 ⊢ (((φ ⋀ ψ ⋀ τ) ⋀ χ) → θ)

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

This theorem is referenced by:  3adantr3 810  fvco 3780  divdiv23t 5794  ltdiv23t 5894  lediv23t 5895  lediv2it 5899  iooss1 6374  ioojoint 6417  expord2t 6605  exple1t 6608  climrecl 7110  climge0 7112  climmullem3 7122  elcls 7701  cnco 7765  dnsconst 7785  metxplem4 7830  elbl2 7836  bl2in 7840  metcnss2 7896  lmuni 7948  lmle 7957  nvmul0or 8268  nvlmle 8329  fh1t 9556  fh2t 9557  cm2jt 9558  pjoi0t 9657  hoadddit 9724  hmopcot 9943

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