Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl2 | GIF version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl2 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 982 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | adantr 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: simpll2 1021 simprl2 1027 simp1l2 1075 simp2l2 1081 simp3l2 1087 3anandirs 1326 rspc3ev 2806 tfisi 4501 brcogw 4708 oawordi 6365 nnmord 6413 nnmword 6414 ac6sfi 6792 unsnfi 6807 unsnfidcel 6809 ordiso2 6920 prarloclemarch2 7227 enq0tr 7242 distrlem4prl 7392 distrlem4pru 7393 ltaprg 7427 aptiprlemu 7448 lelttr 7852 ltletr 7853 readdcan 7902 addcan 7942 addcan2 7943 ltadd2 8181 ltmul1a 8353 ltmul1 8354 divmulassap 8455 divmulasscomap 8456 lemul1a 8616 xrlelttr 9589 xrltletr 9590 xaddass 9652 xleadd1a 9656 xltadd1 9659 xlesubadd 9666 ixxdisj 9686 icoshftf1o 9774 icodisj 9775 lincmb01cmp 9786 iccf1o 9787 fztri3or 9819 ioom 10038 modqmuladdim 10140 modqmuladdnn0 10141 q2submod 10158 modqaddmulmod 10164 exp3val 10295 ltexp2a 10345 exple1 10349 expnbnd 10415 expnlbnd2 10417 expcan 10463 fiprsshashgt1 10563 maxleastb 10986 maxltsup 10990 xrltmaxsup 11026 xrmaxltsup 11027 xrmaxaddlem 11029 xrmaxadd 11030 addcn2 11079 mulcn2 11081 geoisum1c 11289 dvdsval2 11496 dvdsadd2b 11540 dvdsmod 11560 oexpneg 11574 divalglemex 11619 divalg 11621 gcdass 11703 rplpwr 11715 rppwr 11716 lcmass 11766 coprmdvds2 11774 rpmulgcd2 11776 rpdvds 11780 cncongr2 11785 rpexp 11831 znege1 11856 hashgcdlem 11903 ctinf 11943 topssnei 12331 cnptopco 12391 cnconst2 12402 cnptoprest 12408 cnpdis 12411 upxp 12441 bldisj 12570 blgt0 12571 bl2in 12572 blss2ps 12575 blss2 12576 xblm 12586 blssps 12596 blss 12597 xmetresbl 12609 bdbl 12672 bdmopn 12673 metcnp3 12680 metcnp 12681 metcnp2 12682 dvfvalap 12819 dvcnp2cntop 12832 dvcn 12833 |
Copyright terms: Public domain | W3C validator |