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

Theorem animpimp2impd 843
 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 460 . . . . 5 ((𝜓𝜑) → (𝜃 → (𝜂𝜏)))
43a2d 29 . . . 4 ((𝜓𝜑) → ((𝜃𝜂) → (𝜃𝜏)))
51, 4syld 47 . . 3 ((𝜓𝜑) → (𝜒 → (𝜃𝜏)))
65expcom 417 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
76a2d 29 1 (𝜑 → ((𝜓𝜒) → (𝜓 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  seqcl2  13387  seqfveq2  13391  seqshft2  13395  monoord  13399  seqsplit  13402  seqid2  13415  seqhomo  13416  sylow1lem1  18719  imasdsf1olem  22990  ovolicc2lem3  24133  dvnres  24544  cvmliftlem7  32666  cvmliftlem10  32669  monoordxrv  42164  smonoord  43931
 Copyright terms: Public domain W3C validator