Theorem imp4b 365

Description: An importation inference.

Hypothesis

Ref	Expression
imp4.1	⊢ (φ → (ψ → (χ → (θ → τ))))

Assertion

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

Proof of Theorem imp4b

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (φ → (ψ → (χ → (θ → τ))))
2	1	imp4a 364	. 2 ⊢ (φ → (ψ → ((χ ⋀ θ) → τ)))
3	2	imp 350	1 ⊢ ((φ ⋀ ψ) → ((χ ⋀ θ) → τ))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  imp43 370  prth 558  onmindif 3066  eqfnfv 3803  oaordex 4198  nnaordex 4255  nnawordex 4256  pssnn 4544  aceq5 4750  aceq6b 4752  zorn2lem6 4803  alephval3 4914  mulcanpi 5039  ltmpi 5043  genpcd 5121  ltexprlem6 5159  ltexprlem7 5160  reclem3pr 5170  bndndx 6075  iooval2t 6368  basgen2t 7638  blssex 7851  metelcls 7962  mdsymlem3 10327  mdsymlem6 10330  sumdmdlem 10340  cmphmia 10697  cmphmib 10698  iri 10699

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

Copyright terms: Public domain