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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 109 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1020 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  issod  4319  tfisi  4586  tfrlem5  6314  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  ecopovtrn  6631  ecopovtrng  6634  dftap2  7249  addassnqg  7380  ltsonq  7396  ltanqg  7398  ltmnqg  7399  addassnq0  7460  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  lemul1  8548  reapmul1lem  8549  reapmul1  8550  mulcanap  8620  mulcanap2  8621  divassap  8645  divdirap  8652  div11ap  8655  muldivdirap  8662  divcanap5  8669  apmul1  8743  apmul2  8744  ltdiv1  8823  ltmuldiv  8829  ledivmul  8832  lemuldiv  8836  ltdiv2  8842  lediv2  8846  ltdiv23  8847  lediv23  8848  xaddass2  9868  xlt2add  9878  modqdi  10389  expaddzap  10561  expmulzap  10563  leisorel  10812  resqrtcl  11033  xrbdtri  11279  dvdscmulr  11822  dvdsmulcr  11823  dvdsadd2b  11842  dvdsgcd  12007  rpexp12i  12149  pythagtriplem3  12261  pcpremul  12287  pceu  12289  pcqmul  12297  pcqdiv  12301  f1ocpbllem  12713  cmn4  13061  ablsub4  13069  abladdsub4  13070  psmetlecl  13727  xmetlecl  13760
  Copyright terms: Public domain W3C validator