ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpll2 GIF version

Theorem simpll2 986
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll2 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 950 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
21adantr 271 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  fidceq  6665  fidifsnen  6666  en2eqpr  6703  iunfidisj  6735  cauappcvgprlemlol  7303  caucvgprlemlol  7326  caucvgprprlemlol  7354  elfzonelfzo  9790  qbtwnre  9817  hashun  10344  xrmaxltsup  10817  subcn2  10870  divalglemex  11364  divalglemeuneg  11365  dvdslegcd  11398  lcmledvds  11494  iscnp4  12084  cnrest2  12102  blssps  12228  blss  12229  bdbl  12304  metcnp3  12308
  Copyright terms: Public domain W3C validator