MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  animpimp2impd Structured version   Visualization version   GIF version

Theorem animpimp2impd 844
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 457 . . . . 5 ((𝜓𝜑) → (𝜃 → (𝜂𝜏)))
43a2d 29 . . . 4 ((𝜓𝜑) → ((𝜃𝜂) → (𝜃𝜏)))
51, 4syld 47 . . 3 ((𝜓𝜑) → (𝜒 → (𝜃𝜏)))
65expcom 414 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
76a2d 29 1 (𝜑 → ((𝜓𝜒) → (𝜓 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 397
This theorem is referenced by:  seqcl2  13988  seqfveq2  13992  seqshft2  13996  monoord  14000  seqsplit  14003  seqid2  14016  seqhomo  14017  sylow1lem1  19468  imasdsf1olem  23886  ovolicc2lem3  25043  dvnres  25455  cvmliftlem7  34351  cvmliftlem10  34354  monoordxrv  44277  smonoord  46124
  Copyright terms: Public domain W3C validator