ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  animpimp2impd GIF version

Theorem animpimp2impd 554
Description: Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.)
Hypotheses
Ref Expression
animpimp2impd.1 ((𝜓𝜑) → (𝜒 → (𝜃𝜂)))
animpimp2impd.2 ((𝜓 ∧ (𝜑𝜃)) → (𝜂𝜏))
Assertion
Ref Expression
animpimp2impd (𝜑 → ((𝜓𝜒) → (𝜓 → (𝜃𝜏))))

Proof of Theorem animpimp2impd
StepHypRef Expression
1 animpimp2impd.1 . . . 4 ((𝜓𝜑) → (𝜒 → (𝜃𝜂)))
2 animpimp2impd.2 . . . . . 6 ((𝜓 ∧ (𝜑𝜃)) → (𝜂𝜏))
32expr 373 . . . . 5 ((𝜓𝜑) → (𝜃 → (𝜂𝜏)))
43a2d 26 . . . 4 ((𝜓𝜑) → ((𝜃𝜂) → (𝜃𝜏)))
51, 4syld 45 . . 3 ((𝜓𝜑) → (𝜒 → (𝜃𝜏)))
65expcom 115 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
76a2d 26 1 (𝜑 → ((𝜓𝜒) → (𝜓 → (𝜃𝜏))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  seq3fveq2  10412  seq3shft2  10416  seq3split  10422  seq3id2  10452
  Copyright terms: Public domain W3C validator