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

Theorem simp1l 939
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1l (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 106 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 936 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl1l  966  simpr1l  972  simp11l  1026  simp21l  1032  simp31l  1038  en2lp  4305  tfisi  4337  funprg  4976  nnsucsssuc  6101  ecopovtrn  6233  ecopovtrng  6236  addassnqg  6537  distrnqg  6542  ltsonq  6553  ltanqg  6555  ltmnqg  6556  distrnq0  6614  addassnq0  6617  mulasssrg  6900  distrsrg  6901  lttrsr  6904  ltsosr  6906  ltasrg  6912  mulextsr1lem  6921  mulextsr1  6922  axmulass  7004  axdistr  7005  dmdcanap  7772  lt2msq1  7925  ltdiv2  7927  lediv2  7931  modqdi  9336  expaddzaplem  9457  expaddzap  9458  expmulzap  9460  resqrtcl  9848
  Copyright terms: Public domain W3C validator