MPE Home 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 456 . . . . 5 ((𝜓𝜑) → (𝜃 → (𝜂𝜏)))
43a2d 29 . . . 4 ((𝜓𝜑) → ((𝜃𝜂) → (𝜃𝜏)))
51, 4syld 47 . . 3 ((𝜓𝜑) → (𝜒 → (𝜃𝜏)))
65expcom 413 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
76a2d 29 1 (𝜑 → ((𝜓𝜒) → (𝜓 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 396
This theorem is referenced by:  seqcl2  13991  seqfveq2  13995  seqshft2  13999  monoord  14003  seqsplit  14006  seqid2  14019  seqhomo  14020  sylow1lem1  19508  imasdsf1olem  24100  ovolicc2lem3  25269  dvnres  25682  cvmliftlem7  34581  cvmliftlem10  34584  monoordxrv  44491  smonoord  46338
  Copyright terms: Public domain W3C validator