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

Theorem animpimp2impd 846
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  14058  seqfveq2  14062  seqshft2  14066  monoord  14070  seqsplit  14073  seqid2  14086  seqhomo  14087  sylow1lem1  19631  imasdsf1olem  24399  ovolicc2lem3  25568  dvnres  25982  cvmliftlem7  35276  cvmliftlem10  35279  monoordxrv  45432  smonoord  47296
  Copyright terms: Public domain W3C validator