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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 985 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
21adantr 274 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106 This theorem depends on definitions:  df-bi 116  df-3an 964 This theorem is referenced by:  fidceq  6763  fidifsnen  6764  en2eqpr  6801  iunfidisj  6834  ctssdc  6998  cauappcvgprlemlol  7462  caucvgprlemlol  7485  caucvgprprlemlol  7513  elfzonelfzo  10014  qbtwnre  10041  hashun  10558  xrmaxltsup  11034  subcn2  11087  prodmodclem2  11353  divalglemex  11626  divalglemeuneg  11627  dvdslegcd  11660  lcmledvds  11758  iscnp4  12397  cnrest2  12415  blssps  12606  blss  12607  bdbl  12682  metcnp3  12690  addcncntoplem  12730  cdivcncfap  12766
 Copyright terms: Public domain W3C validator