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

Theorem animpimp2impd 847
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 207  df-an 396
This theorem is referenced by:  seqcl2  14061  seqfveq2  14065  seqshft2  14069  monoord  14073  seqsplit  14076  seqid2  14089  seqhomo  14090  sylow1lem1  19616  imasdsf1olem  24383  ovolicc2lem3  25554  dvnres  25967  cvmliftlem7  35296  cvmliftlem10  35299  monoordxrv  45492  smonoord  47358
  Copyright terms: Public domain W3C validator