Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpr1 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 966 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | adantl 275 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: simplr1 1008 simprr1 1014 simp1r1 1062 simp2r1 1068 simp3r1 1074 3anandis 1310 isopolem 5691 caovlem2d 5931 tfrlemibacc 6191 tfrlemibfn 6193 tfr1onlembacc 6207 tfr1onlembfn 6209 tfrcllembacc 6220 tfrcllembfn 6222 eqsupti 6851 prmuloc2 7343 ltntri 7858 elioc2 9687 elico2 9688 elicc2 9689 fseq1p1m1 9842 elfz0ubfz0 9870 ico0 10007 seq3f1olemp 10243 seq3f1oleml 10244 bcval5 10477 isumss2 11130 tanaddap 11373 dvds2ln 11453 divalglemeunn 11545 divalglemex 11546 divalglemeuneg 11547 qredeq 11704 isstructr 11901 icnpimaex 12307 cnptopresti 12334 upxp 12368 psmettri 12426 isxmet2d 12444 xmettri 12468 metrtri 12473 xmetres2 12475 bldisj 12497 blss2ps 12502 blss2 12503 xmstri2 12566 mstri2 12567 xmstri 12568 mstri 12569 xmstri3 12570 mstri3 12571 msrtri 12572 comet 12595 bdbl 12599 xmetxp 12603 dvconst 12757 findset 13070 |
Copyright terms: Public domain | W3C validator |