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

Theorem 3simpb 1146
 Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
Assertion
Ref Expression
3simpb ((𝜑𝜓𝜒) → (𝜑𝜒))

Proof of Theorem 3simpb
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜒) → (𝜑𝜒))
213adant2 1128 1 ((𝜑𝜓𝜒) → (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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  df-3an 1086 This theorem is referenced by:  3adantl2  1164  3adantr2  1167  fpropnf1  7017  cfcof  9734  axcclem  9917  enqeq  10394  ltleletr  10771  ixxssixx  12793  prodmolem2  15337  prodmo  15338  zprod  15339  muldvds1  15682  dvds2add  15691  dvds2sub  15692  dvdstr  15695  initoeu2lem2  17341  pospropd  17810  mndissubm  18038  csrgbinom  19364  smadiadetglem2  21372  ismbf3d  24354  mbfi1flimlem  24422  colinearalg  26803  frusgrnn0  27460  2wlkond  27822  2pthond  27827  2pthon3v  27828  umgr2adedgwlkonALT  27832  vdgn1frgrv2  28180  frgr2wwlkeqm  28215  bnj967  32445  bnj1110  32482  subgrwlk  32610  cgr3permute3  33898  cgr3com  33904  brofs2  33928  bj-idreseq  34857  areacirclem4  35428  paddasslem14  37409  lhpexle1  37584  cdlemk19w  38548  ismrc  40015  iocinico  40535  gneispb  41207  fourierdlem113  43227  sigaras  43835  sigarms  43836  leltletr  44218  lincresunit3lem3  45248  lincresunit3  45255
 Copyright terms: Public domain W3C validator